set all depth to 1

Author: thomas-lamiaux

doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst

@@ -1382,6 +1382,8 @@ with :n:`@reference`, the `All` predicate and its theorem will be looked up with
 
    .. rocqtop:: in reset
 
+      Set All Depth 0.
+
       Inductive prod (A B : Type) : Type :=
       | pair : A -> B -> prod A B.
 

test-suite/output-coqtop/LevelTolerance.out

@@ -14,6 +14,12 @@ Parsing_rect is defined
 Parsing_ind is defined
 Parsing_rec is defined
 Parsing_sind is defined
+Parsing_all is defined
+Parsing_all_rect is defined
+Parsing_all_ind is defined
+Parsing_all_rec is defined
+Parsing_all_sind is defined
+Parsing_all_forall is defined
 
 Rocq < Rocq < 
 Rocq < Rocq < Identifier 'op22' now a keyword

test-suite/output/Search.out

@@ -35,93 +35,94 @@ Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
 Nat.leb: nat -> nat -> bool
 Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
 Number.uint_beq: Number.uint -> Number.uint -> bool
-Number.signed_int_beq: Number.signed_int -> Number.signed_int -> bool
+Nat.ltb: nat -> nat -> bool
 Decimal.signed_int_beq: Decimal.signed_int -> Decimal.signed_int -> bool
 Nat.eqb: nat -> nat -> bool
 Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
-Nat.ltb: nat -> nat -> bool
+Number.signed_int_beq: Number.signed_int -> Number.signed_int -> bool
 Number.number_beq: Number.number -> Number.number -> bool
 Hexadecimal.signed_int_beq:
   Hexadecimal.signed_int -> Hexadecimal.signed_int -> bool
 Hexadecimal.hexadecimal_beq:
   Hexadecimal.hexadecimal -> Hexadecimal.hexadecimal -> bool
 Nat.testbit: nat -> nat -> bool
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+eq_true_rect_r:
+  forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 eq_true_rew_r:
   forall [b : bool] (P : bool -> Type), P b -> eq_true b -> P true
-eq_true_rew:
+bool_sind:
+  forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+eq_true_rect:
   forall P : bool -> Type, P true -> forall [b : bool], eq_true b -> P b
 bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
 eq_true_rec_r:
   forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true
-eq_true_ind:
-  forall P : bool -> Prop, P true -> forall [b : bool], eq_true b -> P b
-eq_true_rect:
-  forall P : bool -> Type, P true -> forall [b : bool], eq_true b -> P b
-eq_true_rect_r:
-  forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true
-eq_true_rec:
-  forall P : bool -> Set, P true -> forall [b : bool], eq_true b -> P b
 eq_true_ind_r:
   forall (P : bool -> Prop) [b : bool], P b -> eq_true b -> P true
-bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
+eq_true_rew:
+  forall P : bool -> Type, P true -> forall [b : bool], eq_true b -> P b
 eq_true_sind:
   forall P : bool -> SProp, P true -> forall [b : bool], eq_true b -> P b
-bool_sind:
-  forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+eq_true_rec:
+  forall P : bool -> Set, P true -> forall [b : bool], eq_true b -> P b
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall [b : bool], eq_true b -> P b
+BoolSpec_all:
+  forall [P : Prop],
+  (P -> Type@{β0 ; _}) ->
+  forall [Q : Prop],
+  (Q -> Type@{β1 ; _}) -> forall [b : bool], BoolSpec P Q b -> Prop
 bool_of_sumbool:
   forall [A B : Prop], {A} + {B} -> {b : bool | if b then A else B}
 sumbool_of_bool: forall b : bool, {b = true} + {b = false}
-Decimal.internal_signed_int_dec_lb:
-  forall x y : Decimal.signed_int, x = y -> Decimal.signed_int_beq x y = true
-Number.internal_signed_int_dec_lb1:
-  forall x y : Number.signed_int, x = y -> Number.signed_int_beq x y = true
-Number.internal_signed_int_dec_bl1:
-  forall x y : Number.signed_int, Number.signed_int_beq x y = true -> x = y
-Decimal.internal_signed_int_dec_bl:
-  forall x y : Decimal.signed_int, Decimal.signed_int_beq x y = true -> x = y
+Number.internal_uint_dec_bl1:
+  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
 Hexadecimal.internal_hexadecimal_dec_lb:
   forall x y : Hexadecimal.hexadecimal,
   x = y -> Hexadecimal.hexadecimal_beq x y = true
+Byte.to_bits:
+  Byte.byte ->
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+Number.internal_uint_dec_lb1:
+  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
+Byte.of_bits:
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
+  Byte.byte
 Hexadecimal.internal_signed_int_dec_lb0:
   forall x y : Hexadecimal.signed_int,
   x = y -> Hexadecimal.signed_int_beq x y = true
+Decimal.internal_signed_int_dec_bl:
+  forall x y : Decimal.signed_int, Decimal.signed_int_beq x y = true -> x = y
+Decimal.internal_decimal_dec_bl:
+  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
+Number.internal_signed_int_dec_lb1:
+  forall x y : Number.signed_int, x = y -> Number.signed_int_beq x y = true
 Number.internal_number_dec_lb:
   forall x y : Number.number, x = y -> Number.number_beq x y = true
+Hexadecimal.internal_hexadecimal_dec_bl:
+  forall x y : Hexadecimal.hexadecimal,
+  Hexadecimal.hexadecimal_beq x y = true -> x = y
+Number.internal_signed_int_dec_bl1:
+  forall x y : Number.signed_int, Number.signed_int_beq x y = true -> x = y
 Hexadecimal.internal_signed_int_dec_bl0:
   forall x y : Hexadecimal.signed_int,
   Hexadecimal.signed_int_beq x y = true -> x = y
-Number.internal_uint_dec_lb1:
-  forall x y : Number.uint, x = y -> Number.uint_beq x y = true
-Number.internal_uint_dec_bl1:
-  forall x y : Number.uint, Number.uint_beq x y = true -> x = y
-Decimal.internal_decimal_dec_bl:
-  forall x y : Decimal.decimal, Decimal.decimal_beq x y = true -> x = y
-Number.internal_number_dec_bl:
-  forall x y : Number.number, Number.number_beq x y = true -> x = y
-Byte.of_bits:
-  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
-  Byte.byte
-Byte.to_bits:
-  Byte.byte ->
-  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+Decimal.internal_signed_int_dec_lb:
+  forall x y : Decimal.signed_int, x = y -> Decimal.signed_int_beq x y = true
 Decimal.internal_decimal_dec_lb:
   forall x y : Decimal.decimal, x = y -> Decimal.decimal_beq x y = true
-Hexadecimal.internal_hexadecimal_dec_bl:
-  forall x y : Hexadecimal.hexadecimal,
-  Hexadecimal.hexadecimal_beq x y = true -> x = y
+Number.internal_number_dec_bl:
+  forall x y : Number.number, Number.number_beq x y = true -> x = y
+eq_true_rew_dep:
+  forall P : forall b : bool, eq_true b -> Type,
+  P true is_eq_true -> forall [b : bool] (e : eq_true b), P b e
 eq_true_rew_fwd_dep:
   forall [b : bool] (H : eq_true b)
     (P : forall b0 : bool, eq_true b0 -> Type),
   P b H -> P true is_eq_true
-eq_true_rew_dep:
-  forall P : forall b : bool, eq_true b -> Type,
-  P true is_eq_true -> forall [b : bool] (e : eq_true b), P b e
-Decimal.internal_uint_dec_bl:
-  forall x : Decimal.uint,
-  (fun x0 : Decimal.uint =>
-   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
 Decimal.internal_uint_dec_lb:
   forall x : Decimal.uint,
   (fun x0 : Decimal.uint =>
@@ -134,6 +135,10 @@ Hexadecimal.internal_uint_dec_bl0:
   forall x : Hexadecimal.uint,
   (fun x0 : Hexadecimal.uint =>
    forall y : Hexadecimal.uint, Hexadecimal.uint_beq x0 y = true -> x0 = y) x
+Decimal.internal_uint_dec_bl:
+  forall x : Decimal.uint,
+  (fun x0 : Decimal.uint =>
+   forall y : Decimal.uint, Decimal.uint_beq x0 y = true -> x0 = y) x
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
@@ -143,21 +148,27 @@ bool_eq_rec:
 bool_eq_ind:
   forall (b : bool) (P : bool -> Prop),
   (b = true -> P true) -> (b = false -> P false) -> P b
-BoolSpec_sind:
-  forall [P Q : Prop] (P0 : bool -> SProp),
-  (P -> P0 true) ->
-  (Q -> P0 false) -> forall [b : bool], BoolSpec P Q b -> P0 b
 BoolSpec_ind:
   forall [P Q : Prop] (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall [b : bool], BoolSpec P Q b -> P0 b
-reflect_ind:
-  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Prop),
+BoolSpec_sind:
+  forall [P Q : Prop] (P0 : bool -> SProp),
+  (P -> P0 true) ->
+  (Q -> P0 false) -> forall [b : bool], BoolSpec P Q b -> P0 b
+BoolSpec_all_forall:
+  forall [P : Prop] (PP : P -> Type@{β0 ; _}),
+  (forall p : P, PP p) ->
+  forall [Q : Prop] (PQ : Q -> Type@{β1 ; _}),
+  (forall q : Q, PQ q) ->
+  forall [b : bool] (b0 : BoolSpec P Q b), BoolSpec_all PP PQ b0
+reflect_rec:
+  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Set),
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
-reflect_sind:
-  forall [P : Prop] (P0 : forall b : bool, reflect P b -> SProp),
+reflect_ind:
+  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Prop),
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
@@ -166,8 +177,8 @@ reflect_rect:
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
-reflect_rec:
-  forall [P : Prop] (P0 : forall b : bool, reflect P b -> Set),
+reflect_sind:
+  forall [P : Prop] (P0 : forall b : bool, reflect P b -> SProp),
   (forall p : P, P0 true (ReflectT P p)) ->
   (forall n : ~ P, P0 false (ReflectF P n)) ->
   forall [b : bool] (r : reflect P b), P0 b r
@@ -179,6 +190,18 @@ bool_choice:
   forall [S : Set] [R1 R2 : S -> Prop],
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
+BoolSpec_all_sind:
+  forall [P : Prop] [PP : P -> Type@{β0 ; _}] [Q : Prop]
+    [PQ : Q -> Type@{β1 ; _}] (P0 : forall b : bool, BoolSpec P Q b -> SProp),
+  (forall p : P, PP p -> P0 true (BoolSpecT Q p)) ->
+  (forall q : Q, PQ q -> P0 false (BoolSpecF P q)) ->
+  forall [b : bool] [b0 : BoolSpec P Q b], BoolSpec_all PP PQ b0 -> P0 b b0
+BoolSpec_all_ind:
+  forall [P : Prop] [PP : P -> Type@{β0 ; _}] [Q : Prop]
+    [PQ : Q -> Type@{β1 ; _}] (P0 : forall b : bool, BoolSpec P Q b -> Prop),
+  (forall p : P, PP p -> P0 true (BoolSpecT Q p)) ->
+  (forall q : Q, PQ q -> P0 false (BoolSpecF P q)) ->
+  forall [b : bool] [b0 : BoolSpec P Q b], BoolSpec_all PP PQ b0 -> P0 b b0
 mult_n_O: forall n : nat, 0 = n * 0
 plus_O_n: forall n : nat, 0 + n = n
 plus_n_O: forall n : nat, n = n + 0

test-suite/output/UnivBinders.out

@@ -203,9 +203,9 @@ block).
 foo@{i} = Type@{M.i} -> Type@{i}
      : Type@{max(M.i+1,i+1)}
 (* i |=  *)
-Type@{u0} -> Type@{UnivBinders.83}
-     : Type@{max(u0+1,UnivBinders.83+1)}
-(* {UnivBinders.83} |=  *)
+Type@{u0} -> Type@{UnivBinders.89}
+     : Type@{max(u0+1,UnivBinders.89+1)}
+(* {UnivBinders.89} |=  *)
 bind_univs.mono = Type@{bind_univs.mono.u}
      : Type@{bind_univs.mono.u+1}
 bind_univs.poly@{u} = Type@{u}

test-suite/output/bug_20242.out

@@ -2,7 +2,7 @@ File "./output/bug_20242.v", line 5, characters 49-60:
 The command has indeed failed with message:
 Signature components for field B do not match: expected type
 "foo@{Type ; A.A.u0} bug_20242.B.A" but found type
-"foo@{SProp ; bug_20242.26} bug_20242.B.A".
+"foo@{SProp ; bug_20242.32} bug_20242.B.A".
 Error: The module B needs to be closed.
 
 

test-suite/output/sort_poly_elim_error.out

@@ -1,7 +1,7 @@
 File "./output/sort_poly_elim_error.v", line 8, characters 0-108:
 The command has indeed failed with message:
 Incorrect elimination of "p" in the inductive type
-"sum@{Prop ; sort_poly_elim_error.23 sort_poly_elim_error.24}":
+"sum@{Prop ; sort_poly_elim_error.35 sort_poly_elim_error.36}":
 the return type has sort "Type" while it should be SProp or Prop.
 Elimination of an inductive object of sort Prop
 is not allowed on a predicate in sort "Type"

vernac/indschemes.ml

@@ -606,7 +606,7 @@ type declare_mind_function = ?all_depth:int ->
 
 (** Depth Generation of all predicate at definition of a new inductive type *)
 let { Goptions.get = default_all_depth } =
-  Goptions.declare_int_option_and_ref ~key:["All";"Depth"] ~value:0 ()
+  Goptions.declare_int_option_and_ref ~key:["All";"Depth"] ~value:1 ()
 
 let default_all_depth kn mib =
   let mib = Global.lookup_mind kn in