aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test-suite/output/Arguments.out8
-rw-r--r--test-suite/output/Arguments_renaming.out10
-rw-r--r--test-suite/output/PrintInfos.out12
-rw-r--r--test-suite/output/Search.out37
-rw-r--r--test-suite/output/SearchHead.out5
-rw-r--r--test-suite/output/SearchPattern.out24
-rw-r--r--test-suite/output/SearchRewrite.out5
7 files changed, 71 insertions, 30 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index f889da4e98..8cf0797b17 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -39,7 +39,7 @@ The reduction tactics unfold Nat.sub when the 1st and
Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
pf :
-forall D1 C1 : Type,
+forall {D1 C1 : Type},
(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
pf is not universe polymorphic
@@ -47,7 +47,7 @@ Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never
The reduction tactics never unfold pf
pf is transparent
Expands to: Constant Arguments.pf
-fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
+fcomp : forall {A B C : Type}, (B -> C) -> (A -> B) -> A -> C
fcomp is not universe polymorphic
Arguments fcomp {A B C}%type_scope _ _ _ /
@@ -75,7 +75,7 @@ The reduction tactics unfold f when the 3rd, 4th and
5th arguments evaluate to a constructor
f is transparent
Expands to: Constant Arguments.S1.S2.f
-f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+f : forall [T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope
@@ -83,7 +83,7 @@ The reduction tactics unfold f when the 4th, 5th and
6th arguments evaluate to a constructor
f is transparent
Expands to: Constant Arguments.S1.f
-f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+f : forall [T1 T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 26ebd8efc3..abc7f0f88e 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -15,7 +15,7 @@ Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
Arguments eq {A}%type_scope
Arguments eq_refl {B}%type_scope {y}, [B] _
-eq_refl : forall (A : Type) (x : A), x = x
+eq_refl : forall {A : Type} {x : A}, x = x
eq_refl is not universe polymorphic
Arguments eq_refl {B}%type_scope {y}, [B] _
@@ -24,7 +24,7 @@ Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x
Arguments myEq _%type_scope
Arguments myrefl {C}%type_scope x : rename
-myrefl : forall (B : Type) (x : A), B -> myEq B x x
+myrefl : forall {B : Type} (x : A), B -> myEq B x x
myrefl is not universe polymorphic
Arguments myrefl {C}%type_scope x : rename
@@ -38,7 +38,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
: forall T : Type, T -> nat -> nat -> nat
Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
-myplus : forall T : Type, T -> nat -> nat -> nat
+myplus : forall {T : Type}, T -> nat -> nat -> nat
myplus is not universe polymorphic
Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
@@ -53,7 +53,7 @@ Inductive myEq (A B : Type) (x : A) : A -> Prop :=
Arguments myEq (_ _)%type_scope
Arguments myrefl A%type_scope {C}%type_scope x : rename
-myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
+myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x
myrefl is not universe polymorphic
Arguments myrefl A%type_scope {C}%type_scope x : rename
@@ -69,7 +69,7 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
: forall T : Type, T -> nat -> nat -> nat
Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
-myplus : forall T : Type, T -> nat -> nat -> nat
+myplus : forall {T : Type}, T -> nat -> nat -> nat
myplus is not universe polymorphic
Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 71d162c314..8fb267e343 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,4 +1,4 @@
-existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
+existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
existT is template universe polymorphic on sigT.u0 sigT.u1
Arguments existT [A]%type_scope _%function_scope
@@ -8,19 +8,19 @@ Inductive sigT (A : Type) (P : A -> Type) : Type :=
Arguments sigT [A]%type_scope _%type_scope
Arguments existT [A]%type_scope _%function_scope
-existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
+existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x}
Argument A is implicit
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
Arguments eq {A}%type_scope
Arguments eq_refl {A}%type_scope {x}, [A] _
-eq_refl : forall (A : Type) (x : A), x = x
+eq_refl : forall {A : Type} {x : A}, x = x
eq_refl is not universe polymorphic
Arguments eq_refl {A}%type_scope {x}, [A] _
Expands to: Constructor Coq.Init.Logic.eq_refl
-eq_refl : forall (A : Type) (x : A), x = x
+eq_refl : forall {A : Type} {x : A}, x = x
When applied to no arguments:
Arguments A, x are implicit and maximally inserted
@@ -65,14 +65,14 @@ bar : foo
bar is not universe polymorphic
Expanded type for implicit arguments
-bar : forall x : nat, x = 0
+bar : forall {x : nat}, x = 0
Arguments bar {x}
Expands to: Constant PrintInfos.bar
*** [ bar : foo ]
Expanded type for implicit arguments
-bar : forall x : nat, x = 0
+bar : forall {x : nat}, x = 0
Arguments bar {x}
Module Coq.Init.Peano
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index ffba1d35cc..9d8e830d64 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -18,6 +18,7 @@ le_sind:
P n ->
(forall m : nat, n <= m -> P m -> P (S m)) ->
forall n0 : nat, n <= n0 -> P n0
+(use "About" for full details on implicit arguments)
false: bool
true: bool
eq_true: bool -> Prop
@@ -37,7 +38,7 @@ Nat.leb: nat -> nat -> bool
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
eq_true_ind_r:
- forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+ forall (P : bool -> Prop) [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
bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
@@ -49,9 +50,9 @@ bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
eq_true_ind:
forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
eq_true_rec_r:
- forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+ forall (P : bool -> Set) [b : bool], P b -> eq_true b -> P true
eq_true_rect_r:
- forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
+ forall (P : bool -> Type) [b : bool], P b -> eq_true b -> P true
bool_sind:
forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
Byte.to_bits:
@@ -62,13 +63,13 @@ Byte.of_bits:
Byte.byte
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
+ forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
BoolSpec_sind:
- forall (P Q : Prop) (P0 : bool -> SProp),
+ 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),
+ forall [P Q : Prop] (P0 : bool -> Prop),
(P -> P0 true) ->
(Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
Byte.to_bits_of_bits:
@@ -76,9 +77,10 @@ Byte.to_bits_of_bits:
b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
Byte.to_bits (Byte.of_bits b) = b
bool_choice:
- forall (S : Set) (R1 R2 : S -> Prop),
+ 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}
+(use "About" for full details on implicit arguments)
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
@@ -104,25 +106,35 @@ f_equal2_mult:
f_equal2_nat:
forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
+(use "About" for full details on implicit arguments)
andb_true_intro:
- forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+ forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
bool_choice:
- forall (S : Set) (R1 R2 : S -> Prop),
+ 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}
+(use "About" for full details on implicit arguments)
andb_true_intro:
- forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+ forall [b1 b2 : bool], b1 = true /\ b2 = true -> (b1 && b2)%bool = true
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+(use "About" for full details on implicit arguments)
andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+(use "About" for full details on implicit arguments)
h: n <> newdef n
h': newdef n <> n
+(use "About" for full details on implicit arguments)
h: n <> newdef n
h': newdef n <> n
+(use "About" for full details on implicit arguments)
h: n <> newdef n
+(use "About" for full details on implicit arguments)
h: n <> newdef n
+(use "About" for full details on implicit arguments)
h: n <> newdef n
h': newdef n <> n
+(use "About" for full details on implicit arguments)
+(use "About" for full details on implicit arguments)
The command has indeed failed with message:
No such goal.
The command has indeed failed with message:
@@ -131,9 +143,14 @@ The command has indeed failed with message:
Query commands only support the single numbered goal selector.
h: P n
h': ~ P n
+(use "About" for full details on implicit arguments)
h: P n
h': ~ P n
+(use "About" for full details on implicit arguments)
h: P n
h': ~ P n
+(use "About" for full details on implicit arguments)
h: P n
+(use "About" for full details on implicit arguments)
h: P n
+(use "About" for full details on implicit arguments)
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 7038eac22c..5627e4bd3c 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -4,6 +4,7 @@ le_S: forall n m : nat, n <= m -> n <= S m
le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
le_n_S: forall n m : nat, n <= m -> S n <= S m
le_S_n: forall n m : nat, S n <= S m -> n <= m
+(use "About" for full details on implicit arguments)
false: bool
true: bool
negb: bool -> bool
@@ -17,6 +18,7 @@ Nat.leb: nat -> nat -> bool
Nat.ltb: nat -> nat -> bool
Nat.testbit: nat -> nat -> bool
Nat.eqb: nat -> nat -> bool
+(use "About" for full details on implicit arguments)
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
@@ -35,5 +37,8 @@ f_equal2_plus:
forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
f_equal2_mult:
forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
+(use "About" for full details on implicit arguments)
h: newdef n
+(use "About" for full details on implicit arguments)
h: P n
+(use "About" for full details on implicit arguments)
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 4cd0ffb1dc..36fc1a5914 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -11,6 +11,7 @@ Nat.leb: nat -> nat -> bool
Nat.ltb: nat -> nat -> bool
Nat.testbit: nat -> nat -> bool
Nat.eqb: nat -> nat -> bool
+(use "About" for full details on implicit arguments)
Nat.two: nat
Nat.one: nat
Nat.zero: nat
@@ -44,8 +45,10 @@ Nat.tail_addmul: nat -> nat -> nat -> nat
Nat.of_uint_acc: Decimal.uint -> nat -> nat
Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-length: forall A : Type, list A -> nat
+length: forall [A : Type], list A -> nat
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+(use "About" for full details on implicit arguments)
+(use "About" for full details on implicit arguments)
Nat.div2: nat -> nat
Nat.sqrt: nat -> nat
Nat.log2: nat -> nat
@@ -74,18 +77,29 @@ Nat.of_uint_acc: Decimal.uint -> nat -> nat
Nat.log2_iter: nat -> nat -> nat -> nat -> nat
Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+(use "About" for full details on implicit arguments)
mult_n_Sm: forall n m : nat, n * m + n = n * S m
+(use "About" for full details on implicit arguments)
iff_refl: forall A : Prop, A <-> A
le_n: forall n : nat, n <= n
-identity_refl: forall (A : Type) (a : A), identity a a
-eq_refl: forall (A : Type) (x : A), x = x
+identity_refl: forall [A : Type] (a : A), identity a a
+eq_refl: forall {A : Type} {x : A}, x = x
Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-conj: forall A B : Prop, A -> B -> A /\ B
-pair: forall A B : Type, A -> B -> A * B
+(use "About" for full details on implicit arguments)
+conj: forall [A B : Prop], A -> B -> A /\ B
+pair: forall {A B : Type}, A -> B -> A * B
Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
+(use "About" for full details on implicit arguments)
+(use "About" for full details on implicit arguments)
h: n <> newdef n
+(use "About" for full details on implicit arguments)
h: n <> newdef n
+(use "About" for full details on implicit arguments)
h: P n
+(use "About" for full details on implicit arguments)
h': ~ P n
+(use "About" for full details on implicit arguments)
h: P n
+(use "About" for full details on implicit arguments)
h: P n
+(use "About" for full details on implicit arguments)
diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out
index 5edea5dff6..3c0880b20c 100644
--- a/test-suite/output/SearchRewrite.out
+++ b/test-suite/output/SearchRewrite.out
@@ -1,5 +1,10 @@
plus_n_O: forall n : nat, n = n + 0
+(use "About" for full details on implicit arguments)
plus_O_n: forall n : nat, 0 + n = n
+(use "About" for full details on implicit arguments)
h: n = newdef n
+(use "About" for full details on implicit arguments)
h: n = newdef n
+(use "About" for full details on implicit arguments)
h: n = newdef n
+(use "About" for full details on implicit arguments)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:57:46 +0000