summaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Arguments.out2
-rw-r--r--test-suite/output/Arguments.v2
-rw-r--r--test-suite/output/ArgumentsScope.v10
-rw-r--r--test-suite/output/Arguments_renaming.out22
-rw-r--r--test-suite/output/Arguments_renaming.v10
-rw-r--r--test-suite/output/Binder.out8
-rw-r--r--test-suite/output/Binder.v7
-rw-r--r--test-suite/output/Cases.out24
-rw-r--r--test-suite/output/Cases.v37
-rw-r--r--test-suite/output/Errors.out3
-rw-r--r--test-suite/output/Errors.v9
-rw-r--r--test-suite/output/Existentials.out3
-rw-r--r--test-suite/output/InitSyntax.out3
-rw-r--r--test-suite/output/Intuition.out2
-rw-r--r--test-suite/output/Naming.out40
-rw-r--r--test-suite/output/Notations.out14
-rw-r--r--test-suite/output/Notations.v3
-rw-r--r--test-suite/output/Notations2.out36
-rw-r--r--test-suite/output/Notations2.v47
-rw-r--r--test-suite/output/Notations3.out100
-rw-r--r--test-suite/output/Notations3.v141
-rw-r--r--test-suite/output/PatternsInBinders.out39
-rw-r--r--test-suite/output/PatternsInBinders.v66
-rw-r--r--test-suite/output/PrintInfos.out34
-rw-r--r--test-suite/output/PrintInfos.v15
-rw-r--r--test-suite/output/PrintModule.out1
-rw-r--r--test-suite/output/PrintModule.v16
-rw-r--r--test-suite/output/Quote.out18
-rw-r--r--test-suite/output/SearchPattern.out2
-rw-r--r--test-suite/output/Tactics.out2
-rw-r--r--test-suite/output/inference.out10
-rw-r--r--test-suite/output/inference.v1
-rw-r--r--test-suite/output/ltac.out34
-rw-r--r--test-suite/output/ltac.v42
-rw-r--r--test-suite/output/onlyprinting.out2
-rw-r--r--test-suite/output/onlyprinting.v5
-rw-r--r--test-suite/output/qualification.out3
-rw-r--r--test-suite/output/qualification.v19
-rw-r--r--test-suite/output/set.out6
-rw-r--r--test-suite/output/simpl.out6
-rw-r--r--test-suite/output/subst.out97
-rw-r--r--test-suite/output/subst.v48
-rw-r--r--test-suite/output/unifconstraints.out65
-rw-r--r--test-suite/output/unifconstraints.v22
44 files changed, 946 insertions, 130 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 2c7b04c6..a2ee2d4c 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -101,4 +101,4 @@ Error: Unknown interpretation for notation "$".
w 3 true = tt
: Prop
The command has indeed failed with message:
-Error: Extra argument _.
+Error: Extra arguments: _, _.
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 05eeaac6..bd924047 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
Arguments fcomp {_ _ _}%type_scope f g x /.
About fcomp.
Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
About volatile.
Set Implicit Arguments.
Section S1.
diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
index 1ff53294..3a90cb79 100644
--- a/test-suite/output/ArgumentsScope.v
+++ b/test-suite/output/ArgumentsScope.v
@@ -11,11 +11,11 @@ About b.
About negb''.
About negb'.
About negb.
-Global Arguments Scope negb'' [ _ ].
-Global Arguments Scope negb' [ _ ].
-Global Arguments Scope negb [ _ ].
-Global Arguments Scope a [ _ ].
-Global Arguments Scope b [ _ ].
+Global Arguments negb'' _ : clear scopes.
+Global Arguments negb' _ : clear scopes.
+Global Arguments negb _ : clear scopes.
+Global Arguments a _ : clear scopes.
+Global Arguments b _ : clear scopes.
About a.
About b.
About negb.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1e3cc37d..b084ad49 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,13 +1,17 @@
The command has indeed failed with message:
Error: To rename arguments the "rename" flag must be specified.
Argument A renamed to B.
-The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
-Argument A renamed to T.
+File "stdin", line 2, characters 0-25:
+Warning: This command is just asserting the names of arguments of identity.
+If this is what you want add ': assert' to silence the warning. If you want
+to clear implicit arguments add ': clear implicits'. If you want to clear
+notation scopes add ': clear scopes' [arguments-assert,vernacular]
@eq_refl
: forall (B : Type) (y : B), y = y
-@eq_refl nat
- : forall x : nat, x = x
+eq_refl
+ : ?y = ?y
+where
+?y : [ |- nat]
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
For eq_refl: Arguments are renamed to B, y
@@ -99,15 +103,15 @@ Expands to: Constant Top.myplus
@myplus
: forall Z : Type, Z -> nat -> nat -> nat
The command has indeed failed with message:
-Error: All arguments lists must declare the same names.
+Error: Argument lists should agree on the names they provide.
The command has indeed failed with message:
-Error: The following arguments are not declared: x.
+Error: Sequences of implicit arguments must be of different lengths.
The command has indeed failed with message:
-Error: Arguments names must be distinct.
+Error: Some argument names are duplicated: F
The command has indeed failed with message:
Error: Argument z cannot be declared implicit.
The command has indeed failed with message:
-Error: Extra argument y.
+Error: Extra arguments: y.
The command has indeed failed with message:
Error: To rename arguments the "rename" flag must be specified.
Argument A renamed to R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index e68fbd69..0cb33134 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,6 +1,6 @@
Fail Arguments eq_refl {B y}, [B] y.
-Fail Arguments identity T _ _.
-Arguments eq_refl A x.
+Arguments identity A _ _.
+Arguments eq_refl A x : assert.
Arguments eq_refl {B y}, [B] y : rename.
Check @eq_refl.
@@ -46,9 +46,9 @@ About myplus.
Check @myplus.
Fail Arguments eq_refl {F g}, [H] k.
-Fail Arguments eq_refl {F}, [F].
-Fail Arguments eq_refl {F F}, [F] F.
-Fail Arguments eq {F} x [z].
+Fail Arguments eq_refl {F}, [F] : rename.
+Fail Arguments eq_refl {F F}, [F] F : rename.
+Fail Arguments eq {F} x [z] : rename.
Fail Arguments eq {F} x z y.
Fail Arguments eq {R} s t.
diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out
new file mode 100644
index 00000000..34558e9a
--- /dev/null
+++ b/test-suite/output/Binder.out
@@ -0,0 +1,8 @@
+foo = fun '(x, y) => x + y
+ : nat * nat -> nat
+forall '(a, b), a /\ b
+ : Prop
+foo = λ '(x, y), x + y
+ : nat * nat → nat
+∀ '(a, b), a ∧ b
+ : Prop
diff --git a/test-suite/output/Binder.v b/test-suite/output/Binder.v
new file mode 100644
index 00000000..9aced9f6
--- /dev/null
+++ b/test-suite/output/Binder.v
@@ -0,0 +1,7 @@
+Definition foo '(x,y) := x + y.
+Print foo.
+Check forall '(a,b), a /\ b.
+
+Require Import Utf8.
+Print foo.
+Check forall '(a,b), a /\ b.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 09f032d4..8ce6f979 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,6 +6,8 @@ fix F (t : t) : P t :=
end
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
+
+Argument scopes are [function_scope function_scope _]
= fun d : TT => match d with
| @CTT _ _ b => b
end
@@ -24,7 +26,7 @@ match Nat.eq_dec x y with
end
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
-Argument scopes are [nat_scope nat_scope _ _ _]
+Argument scopes are [nat_scope nat_scope function_scope _ _]
foo =
fix foo (A : Type) (l : list A) {struct l} : option A :=
match l with
@@ -48,9 +50,25 @@ f =
fun H : B =>
match H with
| AC x =>
- (let b0 := b in
- if b0 as b return (P b -> True)
+ let b0 := b in
+ (if b0 as b return (P b -> True)
then fun _ : P true => Logic.I
else fun _ : P false => Logic.I) x
end
: B -> True
+The command has indeed failed with message:
+Non exhaustive pattern-matching: no clause found for pattern
+gadtTy _ _
+The command has indeed failed with message:
+In environment
+texpDenote : forall t : type, texp t -> typeDenote t
+t : type
+e : texp t
+t1 : type
+t2 : type
+t0 : type
+b : tbinop t1 t2 t0
+e1 : texp t1
+e2 : texp t2
+The term "0" has type "nat" while it is expected to have type
+ "typeDenote t0".
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4116a5eb..40748964 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -66,14 +66,43 @@ Print foo'.
(* Was bug #3293 (eta-expansion at "match" printing time was failing because
of let-in's interpreted as being part of the expansion) *)
-Variable b : bool.
-Variable P : bool -> Prop.
+Axiom b : bool.
+Axiom P : bool -> Prop.
Inductive B : Prop := AC : P b -> B.
Definition f : B -> True.
Proof.
-intros [].
-destruct b as [|] ; intros _ ; exact Logic.I.
+intros [x].
+destruct b as [|] ; exact Logic.I.
Defined.
Print f.
+
+(* Was enhancement request #5142 (error message reported on the most
+ general return clause heuristic) *)
+
+Inductive gadt : Type -> Type :=
+| gadtNat : nat -> gadt nat
+| gadtTy : forall T, T -> gadt T.
+
+Fail Definition gadt_id T (x: gadt T) : gadt T :=
+ match x with
+ | gadtNat n => gadtNat n
+ end.
+
+(* A variant of #5142 (see Satrajit Roy's example on coq-club (Oct 17, 2016)) *)
+
+Inductive type:Set:=Nat.
+Inductive tbinop:type->type->type->Set:= TPlus : tbinop Nat Nat Nat.
+Inductive texp:type->Set:=
+ |TNConst:nat->texp Nat
+ |TBinop:forall t1 t2 t, tbinop t1 t2 t->texp t1->texp t2->texp t.
+Definition typeDenote(t:type):Set:= match t with Nat => nat end.
+
+(* We expect a failure on TBinop *)
+Fail Fixpoint texpDenote t (e:texp t):typeDenote t:=
+ match e with
+ | TNConst n => n
+ | TBinop t1 t2 _ b e1 e2 => O
+ end.
+
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 6354ad46..06a6b2d1 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -5,3 +5,6 @@ Unable to unify "nat" with "True".
The command has indeed failed with message:
In nested Ltac calls to "f" and "apply x", last call failed.
Unable to unify "nat" with "True".
+The command has indeed failed with message:
+Ltac call to "instantiate ( (ident) := (lglob) )" failed.
+Error: Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 352c8738..424d2480 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -16,3 +16,12 @@ Goal True.
Fail simpl; apply 0.
Fail simpl; f 0.
Abort.
+
+(* Test instantiate error messages *)
+
+Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1.
+intros T1 P1 H1.
+eexists ?[x].
+destruct H1 as [x1 H1].
+Fail instantiate (x:=projT1 x1).
+Abort.
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 52e1e0ed..9680d2bb 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,5 +1,4 @@
-Existential 1 =
-?Goal1 : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
+Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m]
Existential 2 =
?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used)
Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y]
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index bbfd3405..c17c63e7 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -4,7 +4,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
For sig2: Argument A is implicit
For exist2: Argument A is implicit
For sig2: Argument scopes are [type_scope type_scope type_scope]
-For exist2: Argument scopes are [type_scope _ _ _ _ _]
+For exist2: Argument scopes are [type_scope function_scope function_scope _ _
+ _]
exists x : nat, x = x
: Prop
fun b : bool => if b then b else b
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
index e99d9fde..f2bf25ca 100644
--- a/test-suite/output/Intuition.out
+++ b/test-suite/output/Intuition.out
@@ -3,4 +3,4 @@
m, n : Z
H : (m >= n)%Z
============================
- (m >= m)%Z
+ (m >= m)%Z
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index f0d2562e..c142d28e 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -2,40 +2,40 @@
x3 : nat
============================
- forall x x1 x4 x0 : nat,
- (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
+ forall x x1 x4 x0 : nat,
+ (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
1 subgoal
x3, x, x1, x4, x0 : nat
H : forall x x3 : nat, x + x1 = x4 + x3
============================
- x + x1 = x4 + x0
+ x + x1 = x4 + x0
1 subgoal
x3 : nat
============================
- forall x x1 x4 x0 : nat,
- (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
- x + x1 = x4 + x0 -> foo (S x)
+ forall x x1 x4 x0 : nat,
+ (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
+ x + x1 = x4 + x0 -> foo (S x)
1 subgoal
x3 : nat
============================
- forall x x1 x4 x0 : nat,
- (forall x2 x5 : nat,
- x2 + x1 = x4 + x5 ->
- forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
- x + x1 = x4 + x0 ->
- forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+ forall x x1 x4 x0 : nat,
+ (forall x2 x5 : nat,
+ x2 + x1 = x4 + x5 ->
+ forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+ x + x1 = x4 + x0 ->
+ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, x, x1, x4, x0 : nat
============================
- (forall x2 x5 : nat,
- x2 + x1 = x4 + x5 ->
- forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
- x + x1 = x4 + x0 ->
- forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+ (forall x2 x5 : nat,
+ x2 + x1 = x4 + x5 ->
+ forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+ x + x1 = x4 + x0 ->
+ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, x, x1, x4, x0 : nat
@@ -44,7 +44,7 @@
forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
H0 : x + x1 = x4 + x0
============================
- forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, x, x1, x4, x0 : nat
@@ -54,10 +54,10 @@
H0 : x + x1 = x4 + x0
x5, x6, x7, S : nat
============================
- x5 + S = x6 + x7 + Datatypes.S x
+ x5 + S = x6 + x7 + Datatypes.S x
1 subgoal
x3, a : nat
H : a = 0 -> forall a : nat, a = 0
============================
- a = 0
+ a = 0
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b1558dab..26eaca82 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,14 +111,14 @@ fun x : option Z => match x with
| NONE2 => 0
end
: option Z -> Z
-fun x : list ?T1 => match x with
- | NIL => NONE2
- | (_ :') t => SOME2 t
- end
- : list ?T1 -> option (list ?T1)
+fun x : list ?T => match x with
+ | NIL => NONE2
+ | (_ :') t => SOME2 t
+ end
+ : list ?T -> option (list ?T)
where
-?T1 : [x : list ?T1 x1 : list ?T1 x0 := x1 : list ?T1 |- Type] (x, x1,
- x0 cannot be used)
+?T : [x : list ?T x1 : list ?T x0 := x1 : list ?T |- Type] (x, x1,
+ x0 cannot be used)
s
: s
10
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index adba688e..2ccca829 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -133,8 +133,7 @@ Fail Notation "( x , y , .. , z )" := (pair x (pair y z)).
Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..).
(* Right-unbound variable *)
-(* Now allowed with an only parsing restriction *)
-Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..).
+Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..) (only parsing).
(* Not the right kind of recursive pattern *)
Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)).
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 58ec1de5..ad60aecc 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -12,7 +12,7 @@ let '(a, _, _) := (2, 3, 4) in a
: nat
exists myx y : bool, myx = y
: Prop
-fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
+fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
: (nat -> nat -> Prop) -> nat -> Prop
∃ n p : nat, n + p = 0
: Prop
@@ -50,3 +50,37 @@ end
: nat -> nat
# _ : nat => 2
: nat -> nat
+# x : nat => # H : x <= 0 => exist (le x) 0 H
+ : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
+exist (Q x) y conj
+ : {x0 : A | Q x x0}
+% i
+ : nat -> nat
+% j
+ : nat -> nat
+{1, 2}
+ : nat -> Prop
+a#
+ : Set
+a#
+ : Set
+a≡
+ : Set
+a≡
+ : Set
+.≡
+ : Set
+.≡
+ : Set
+.a#
+ : Set
+.a#
+ : Set
+.a≡
+ : Set
+.a≡
+ : Set
+.α
+ : Set
+.α
+ : Set
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e53c94ef..ceb29d1b 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -68,6 +68,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
(* In practice, only the printing rule is used here *)
(* Note: does not work for pattern *)
+Module A.
Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
Check fun f x => f x + S x.
@@ -77,6 +78,7 @@ Notation plus2 n := (S (S n)).
(* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
Print plus2.
Check fun n => match n with list1 => 0 | _ => 2 end.
+End A.
(* This one is not fully satisfactory because binders in the same type
are re-factorized and parentheses are needed even for atomic binder
@@ -98,3 +100,48 @@ Notation "# x : T => t" := (fun x : T => t)
Check # x : nat => x.
Check # _ : nat => 2.
+
+(* Check bug 4677 *)
+Check fun x (H:le x 0) => exist (le x) 0 H.
+
+Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
+Check (exist (Q x) y conj).
+
+(* Check bug #4854 *)
+Notation "% i" := (fun i : nat => i) (at level 0, i ident).
+Check %i.
+Check %j.
+
+(* Check bug raised on coq-club on Sep 12, 2016 *)
+
+Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))).
+Check ({1, 2}).
+
+(**********************************************************************)
+(* Check notations of the form ".a", ".a≡", "a≡" *)
+(* Only "a#", "a≡" and ".≡" were working properly for parsing. The *)
+(* other ones were working only for printing. *)
+
+Notation "a#" := nat.
+Check nat.
+Check a#.
+
+Notation "a≡" := nat.
+Check nat.
+Check a≡.
+
+Notation ".≡" := nat.
+Check nat.
+Check .≡.
+
+Notation ".a#" := nat.
+Check nat.
+Check .a#.
+
+Notation ".a≡" := nat.
+Check nat.
+Check .a≡.
+
+Notation ".α" := nat.
+Check nat.
+Check .α.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
new file mode 100644
index 00000000..360f3796
--- /dev/null
+++ b/test-suite/output/Notations3.out
@@ -0,0 +1,100 @@
+[<0, 2 >]
+ : nat * nat * (nat * nat)
+[<0, 2 >]
+ : nat * nat * (nat * nat)
+(0, 2, (2, 2))
+ : nat * nat * (nat * nat)
+pair (pair O (S (S O))) (pair (S (S O)) O)
+ : prod (prod nat nat) (prod nat nat)
+<< 0, 2, 4 >>
+ : nat * nat * nat * (nat * (nat * nat))
+<< 0, 2, 4 >>
+ : nat * nat * nat * (nat * (nat * nat))
+(0, 2, 4, (2, (2, 0)))
+ : nat * nat * nat * (nat * (nat * nat))
+(0, 2, 4, (0, (2, 4)))
+ : nat * nat * nat * (nat * (nat * nat))
+pair (pair (pair O (S (S O))) (S (S (S (S O)))))
+ (pair (S (S (S (S O)))) (pair (S (S O)) O))
+ : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
+ETA x y : nat, Nat.add
+ : nat -> nat -> nat
+ETA x y : nat, Nat.add
+ : nat -> nat -> nat
+ETA x y : nat, Nat.add
+ : nat -> nat -> nat
+fun x y : nat => Nat.add x y
+ : forall (_ : nat) (_ : nat), nat
+ETA x y : nat, le_S
+ : forall x y : nat, x <= y -> x <= S y
+fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
+ : (forall x : nat * (bool * unit), ?T) ->
+ forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
+where
+?T : [x : nat * (bool * unit) |- Type]
+fun f : forall x : bool * (nat * unit), ?T =>
+CURRYINV (x : nat) (y : bool), f
+ : (forall x : bool * (nat * unit), ?T) ->
+ forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))}
+where
+?T : [x : bool * (nat * unit) |- Type]
+fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f
+ : (forall x : unit * nat * bool, ?T) ->
+ forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)}
+where
+?T : [x : unit * nat * bool |- Type]
+fun f : forall x : unit * bool * nat, ?T =>
+CURRYINVLEFT (x : nat) (y : bool), f
+ : (forall x : unit * bool * nat, ?T) ->
+ forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)}
+where
+?T : [x : unit * bool * nat |- Type]
+forall n : nat, {#n | 1 > n}
+ : Prop
+forall x : nat, {|x | x > 0|}
+ : Prop
+exists2 x : nat, x = 1 & x = 2
+ : Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + z = 0) z y x)
+ : nat -> Prop
+fun n : nat =>
+foo2 n (fun a b c : nat => (fun _ _ _ : nat => a + b + c = 0) c b a)
+ : nat -> Prop
+fun n : nat =>
+foo2 n (fun n0 y z : nat => (fun _ _ _ : nat => n0 + y + z = 0) z y n0)
+ : nat -> Prop
+fun n : nat =>
+foo2 n (fun x n0 z : nat => (fun _ _ _ : nat => x + n0 + z = 0) z n0 x)
+ : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y n0 : nat => (fun _ _ _ : nat => x + y + n0 = 0) n0 y x)
+ : nat -> Prop
+fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
+ : nat -> Prop
+fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
+ : nat -> Prop
+fun n : nat => {|n, n0 | fun _ _ _ : nat => n + n0 = 0 |}_2
+ : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
+ : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
+ : nat -> Prop
+fun n : nat => {|n, fun _ : nat => 0 = 0 |}_3
+ : nat -> Prop
+fun n : nat => {|n, fun _ : nat => n = 0 |}_3
+ : nat -> Prop
+fun n : nat => foo3 n (fun x _ : nat => ETA z : nat, (fun _ : nat => x = 0))
+ : nat -> Prop
+fun n : nat => {|n, fun _ : nat => 0 = 0 |}_4
+ : nat -> Prop
+fun n : nat => {|n, fun _ : nat => n = 0 |}_4
+ : nat -> Prop
+fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0))
+ : nat -> Prop
+fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
+ : nat -> Prop
+tele (t : Type) '(y, z) (x : t0) := tt
+ : forall t : Type, nat * nat -> t -> fpack
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
new file mode 100644
index 00000000..4b8bfe31
--- /dev/null
+++ b/test-suite/output/Notations3.v
@@ -0,0 +1,141 @@
+(**********************************************************************)
+(* Check printing of notations with several instances of a recursive pattern *)
+(* Was wrong but I could not trigger a problem due to the collision between *)
+(* different instances of ".." *)
+
+Notation "[< x , y , .. , z >]" := (pair (.. (pair x y) ..) z,pair y ( .. (pair z x) ..)).
+Check [<0,2>].
+Check ((0,2),(2,0)).
+Check ((0,2),(2,2)).
+Unset Printing Notations.
+Check [<0,2>].
+Set Printing Notations.
+
+Notation "<< x , y , .. , z >>" := ((.. (x,y) .., z),(z, .. (y,x) ..)).
+Check <<0,2,4>>.
+Check (((0,2),4),(4,(2,0))).
+Check (((0,2),4),(2,(2,0))).
+Check (((0,2),4),(0,(2,4))).
+Unset Printing Notations.
+Check <<0,2,4>>.
+Set Printing Notations.
+
+(**********************************************************************)
+(* Check notations with recursive notations both in binders and terms *)
+
+Notation "'ETA' x .. y , f" :=
+ (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+ (at level 200, x binder, y binder).
+Check ETA (x:nat) (y:nat), Nat.add.
+Check ETA (x y:nat), Nat.add.
+Check ETA x y, Nat.add.
+Unset Printing Notations.
+Check ETA (x:nat) (y:nat), Nat.add.
+Set Printing Notations.
+Check ETA x y, le_S.
+
+Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..)
+ (at level 200, x binder, y binder).
+Check fun f => CURRY (x:nat) (y:bool), f.
+
+Notation "'CURRYINV' x .. y , f" := (fun x => .. (fun y => f (y, .. (x,tt) ..)) ..)
+ (at level 200, x binder, y binder).
+Check fun f => CURRYINV (x:nat) (y:bool), f.
+
+Notation "'CURRYLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,x) .., y)) ..)
+ (at level 200, x binder, y binder).
+Check fun f => CURRYLEFT (x:nat) (y:bool), f.
+
+Notation "'CURRYINVLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,y) .., x)) ..)
+ (at level 200, x binder, y binder).
+Check fun f => CURRYINVLEFT (x:nat) (y:bool), f.
+
+(**********************************************************************)
+(* Notations with variables bound both as a term and as a binder *)
+(* This is #4592 *)
+
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
+Check forall n:nat, {# n | 1 > n}.
+
+Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
+Notation "{| x | P |}" := (foo x (fun x => P)).
+Check forall x:nat, {| x | x > 0 |}.
+
+Check ex2 (fun x => x=1) (fun x0 => x0=2).
+
+(* Other tests about alpha-conversions: the following notation
+ contains all three kinds of bindings:
+
+ - x is bound in the lhs as a term and a binder: its name is forced
+ by its position as a term; it can bind variables in P
+ - y is bound in the lhs as a binder only: its name is given by its
+ name as a binder in the term to display; it can bind variables in P
+ - z is a binder local to the rhs; it cannot bind a variable in P
+*)
+
+Parameter foo2 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , y | P |}_2" := (foo2 x (fun x y z => P z y x)).
+
+(* Not printable: z (resp c, n) occurs in P *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+z=0) z y x).
+Check fun n => foo2 n (fun a b c => (fun _ _ _ => a+b+c=0) c b a).
+Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y+z=0) z y n).
+Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n+z=0) z n x).
+Check fun n => foo2 n (fun x y n => (fun _ _ _ => x+y+n=0) n y x).
+
+(* Printable *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y=0) z y x).
+Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y=0) z y n).
+Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n=0) z n x).
+
+(* Not printable: renaming x into n would bind the 2nd occurrence of n *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
+
+(* Other tests *)
+Parameter foo3 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , P |}_3" := (foo3 x (fun x x x => P x)).
+
+(* Printable *)
+Check fun n : nat => foo3 n (fun x y z => (fun _ => 0=0) z).
+Check fun n => foo3 n (fun x y z => (fun _ => z=0) z).
+
+(* Not printable: renaming z in n would hide the renaming of x into n *)
+Check fun n => foo3 n (fun x y z => (fun _ => x=0) z).
+
+(* Other tests *)
+Parameter foo4 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , P |}_4" := (foo4 x (fun x _ z => P z)).
+
+(* Printable *)
+Check fun n : nat => foo4 n (fun x y z => (fun _ => 0=0) z).
+Check fun n => foo4 n (fun x y z => (fun _ => x=0) z).
+
+(* Not printable: y, z not allowed to occur in P *)
+Check fun n => foo4 n (fun x y z => (fun _ => z=0) z).
+Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
+
+(**********************************************************************)
+(* Test printing of #4932 *)
+
+Inductive ftele : Type :=
+| fb {T:Type} : T -> ftele
+| fr {T} : (T -> ftele) -> ftele.
+
+Fixpoint args ftele : Type :=
+ match ftele with
+ | fb _ => unit
+ | fr f => sigT (fun t => args (f t))
+ end.
+
+Definition fpack := sigT args.
+Definition pack fp fa : fpack := existT _ fp fa.
+
+Notation "'tele' x .. z := b" :=
+ (fun x => .. (fun z =>
+ pack (fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
+ (existT _ x .. (existT _ z tt) .. )
+ ) ..)
+ (at level 85, x binder, z binder).
+
+Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
new file mode 100644
index 00000000..c012a86b
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.out
@@ -0,0 +1,39 @@
+swap = fun '(x, y) => (y, x)
+ : A * B -> B * A
+fun '(x, y) => (y, x)
+ : A * B -> B * A
+forall '(x, y), swap (x, y) = (y, x)
+ : Prop
+proj_informative = fun '(exist _ x _) => x : A
+ : {x : A | P x} -> A
+foo = fun '(Bar n b tt p) => if b then n + p else n - p
+ : Foo -> nat
+baz =
+fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
+ : Foo -> Foo -> nat
+swap =
+fun (A B : Type) '(x, y) => (y, x)
+ : forall A B : Type, A * B -> B * A
+
+Arguments A, B are implicit and maximally inserted
+Argument scopes are [type_scope type_scope _]
+fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
+ : forall A B : Type, A * B -> Prop
+forall (A B : Type) '(x, y), swap (x, y) = (y, x)
+ : Prop
+exists '(x, y), swap (x, y) = (y, x)
+ : Prop
+exists '(x, y) '(z, w), swap (x, y) = (z, w)
+ : Prop
+λ '(x, y), (y, x)
+ : A * B → B * A
+∀ '(x, y), swap (x, y) = (y, x)
+ : Prop
+both_z =
+fun pat : nat * nat =>
+let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p)
+ : forall pat : nat * nat, F pat
+fun '(x, y) '(z, t) => swap (x, y) = (z, t)
+ : A * B -> B * A -> Prop
+forall '(x, y) '(z, t), swap (x, y) = (z, t)
+ : Prop
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
new file mode 100644
index 00000000..6fa357a9
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.v
@@ -0,0 +1,66 @@
+Require Coq.Unicode.Utf8.
+
+(** The purpose of this file is to test printing of the destructive
+ patterns used in binders ([fun] and [forall]). *)
+
+Parameters (A B : Type) (P:A->Prop).
+
+Definition swap '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check fun '((x,y) : A*B) => (y,x).
+
+Check forall '(x,y), swap (x,y) = (y,x).
+
+Definition proj_informative '(exist _ x _ : { x:A | P x }) : A := x.
+Print proj_informative.
+
+Inductive Foo := Bar : nat -> bool -> unit -> nat -> Foo.
+Definition foo '(Bar n b tt p) :=
+ if b then n+p else n-p.
+Print foo.
+
+Definition baz '(Bar n1 b1 tt p1) '(Bar n2 b2 tt p2) := n1+p1.
+Print baz.
+
+Module WithParameters.
+
+Definition swap {A B} '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check fun (A B:Type) '((x,y) : A*B) => swap (x,y) = (y,x).
+Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x).
+
+Check exists '((x,y):A*A), swap (x,y) = (y,x).
+Check exists '((x,y):A*A) '(z,w), swap (x,y) = (z,w).
+
+End WithParameters.
+
+(** Some test involving unicode notations. *)
+Module WithUnicode.
+
+ Import Coq.Unicode.Utf8.
+
+ Check λ '((x,y) : A*B), (y,x).
+ Check ∀ '(x,y), swap (x,y) = (y,x).
+
+End WithUnicode.
+
+(** * Suboptimal printing *)
+
+Module Suboptimal.
+
+(** This test shows an example which exposes the [let] introduced by
+ the pattern notation in binders. *)
+
+Inductive Fin (n:nat) := Z : Fin n.
+Definition F '(n,p) : Type := (Fin n * Fin p)%type.
+Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
+Print both_z.
+
+(** Test factorization of binders *)
+
+Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
+Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
+
+End Suboptimal.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ba076f05..1307a8f2 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -2,7 +2,7 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
existT is template universe polymorphic
Argument A is implicit
-Argument scopes are [type_scope _ _ _]
+Argument scopes are [type_scope function_scope _ _]
Expands to: Constructor Coq.Init.Specif.existT
Inductive sigT (A : Type) (P : A -> Type) : Type :=
existT : forall x : A, P x -> {x : A & P x}
@@ -10,7 +10,7 @@ Inductive sigT (A : Type) (P : A -> Type) : Type :=
For sigT: Argument A is implicit
For existT: Argument A is implicit
For sigT: Argument scopes are [type_scope type_scope]
-For existT: Argument scopes are [type_scope _ _ _]
+For existT: Argument scopes are [type_scope function_scope _ _]
existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
Argument A is implicit
@@ -66,14 +66,6 @@ For le_S: Argument n is implicit and maximally inserted
For le: Argument scopes are [nat_scope nat_scope]
For le_n: Argument scope is [nat_scope]
For le_S: Argument scopes are [nat_scope nat_scope _]
-Inductive le (n : nat) : nat -> Prop :=
- le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
-
-For le_S: Argument m is implicit
-For le_S: Argument n is implicit and maximally inserted
-For le: Argument scopes are [nat_scope nat_scope]
-For le_n: Argument scope is [nat_scope]
-For le_S: Argument scopes are [nat_scope nat_scope _]
comparison : Set
Expands to: Inductive Coq.Init.Datatypes.comparison
@@ -92,19 +84,6 @@ Expanded type for implicit arguments
bar : forall x : nat, x = 0
Argument x is implicit and maximally inserted
-bar : foo
-
-Expanded type for implicit arguments
-bar : forall x : nat, x = 0
-
-Argument x is implicit and maximally inserted
-Expands to: Constant Top.bar
-*** [ bar : foo ]
-
-Expanded type for implicit arguments
-bar : forall x : nat, x = 0
-
-Argument x is implicit and maximally inserted
Module Coq.Init.Peano
Notation existS2 := existT2
Expands to: Notation Coq.Init.Specif.existS2
@@ -117,15 +96,6 @@ For eq_refl, when applied to 1 argument:
Argument A is implicit and maximally inserted
For eq: Argument scopes are [type_scope _ _]
For eq_refl: Argument scopes are [type_scope _]
-Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
-
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
- Arguments A, x are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
- Argument A is implicit and maximally inserted
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
n:nat
Hypothesis of the goal context.
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 3c623346..08918981 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -12,10 +12,7 @@ Print Implicit Nat.add.
About plus_n_O.
-Implicit Arguments le_S [[n] m].
-Print le_S.
-
-Arguments le_S {n} [m] _. (* Test new syntax *)
+Arguments le_S {n} [m] _.
Print le_S.
About comparison.
@@ -23,21 +20,15 @@ Print comparison.
Definition foo := forall x, x = 0.
Parameter bar : foo.
-Implicit Arguments bar [x].
-About bar.
-Print bar.
-Arguments bar [x]. (* Test new syntax *)
+Arguments bar [x].
About bar.
Print bar.
About Peano. (* Module *)
About existS2. (* Notation *)
-Implicit Arguments eq_refl [[A] [x]] [[A]].
-Print eq_refl.
-
-Arguments eq_refl {A} {x}, {A} x. (* Test new syntax *)
+Arguments eq_refl {A} {x}, {A} x.
Print eq_refl.
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index db464fd0..751d5fcc 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -2,3 +2,4 @@ Module N : S with Definition T := nat := M
Module N : S with Module T := K := M
+Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 999d9a98..5f30f7cd 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -32,3 +32,19 @@ Module N : S with Module T := K := M.
Print Module N.
End BAR.
+
+Module QUX.
+
+Module Type Test.
+ Parameter t : Type.
+End Test.
+
+Module Type Func (T:Test).
+ Parameter x : T.t.
+End Func.
+
+Module Shortest_path (T : Test).
+Print Func.
+End Shortest_path.
+
+End QUX.
diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out
index ca7fc362..998eb37c 100644
--- a/test-suite/output/Quote.out
+++ b/test-suite/output/Quote.out
@@ -8,17 +8,17 @@
H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
B
============================
- interp_f
- (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
- (f_and (f_atom (Left_idx End_idx))
- (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
- (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
+ interp_f
+ (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
+ (f_and (f_atom (Left_idx End_idx))
+ (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
+ (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
1 subgoal
H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
B
============================
- interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
- (f_and (f_const A)
- (f_and (f_or (f_atom End_idx) (f_const A))
- (f_or (f_const A) (f_not (f_atom End_idx)))))
+ interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
+ (f_and (f_const A)
+ (f_and (f_or (f_atom End_idx) (f_const A))
+ (f_or (f_const A) (f_not (f_atom End_idx)))))
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 1eb7eca8..f3c12eff 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -40,7 +40,6 @@ Nat.land: nat -> nat -> nat
Nat.lor: nat -> nat -> nat
Nat.ldiff: nat -> nat -> nat
Nat.lxor: nat -> nat -> nat
-
S: nat -> nat
Nat.succ: nat -> nat
Nat.pred: nat -> nat
@@ -74,7 +73,6 @@ le_n: forall n : nat, n <= n
pair: forall A B : Type, A -> B -> A * B
conj: forall A B : Prop, A -> B -> A /\ B
Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-
h: n <> newdef n
h: n <> newdef n
h: P n
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 9949658c..239edd1d 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,4 +1,4 @@
Ltac f H := split; [ a H | e H ]
Ltac g := match goal with
- | |- context [if ?X then _ else _] => case X
+ | |- context [ if ?X then _ else _ ] => case X
end
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index f2d14477..576fbd7c 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
: option L -> option L
fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
: forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x := A n in ?y ?y0 : T n
+fun n : nat => let x := A n : T n in ?y ?y0 : T n
: forall n : nat, T n
where
-?y : [n : nat x := A n : T n |- ?T0 -> T n]
-?y0 : [n : nat x := A n : T n |- ?T0]
+?y : [n : nat x := A n : T n |- ?T -> T n]
+?y0 : [n : nat x := A n : T n |- ?T]
fun n : nat => ?y ?y0 : T n
: forall n : nat, T n
where
-?y : [n : nat |- ?T0 -> T n]
-?y0 : [n : nat |- ?T0]
+?y : [n : nat |- ?T -> T n]
+?y0 : [n : nat |- ?T]
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index cd9a4a12..1825db16 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -14,6 +14,7 @@ Definition P (e:option L) :=
Print P.
(* Check that plus is folded even if reduction is involved *)
+Set Refolding Reduction.
Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index d003c70d..1ff09e3a 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,34 @@
The command has indeed failed with message:
-Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Error:
+Ltac variable y depends on pattern variable name z which is not bound in current context.
+Ltac f x y z :=
+ symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
+ dependent z
+The command has indeed failed with message:
+In nested Ltac calls to "g1" and "refine (uconstr)", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call
+failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call
+failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call
+failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
+Error: No primitive equality found.
+The command has indeed failed with message:
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
+Error: No primitive equality found.
+Hx
+nat
+nat
+0
+0
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7..76c37625 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,45 @@ lazymatch goal with
| H1 : HT |- _ => idtac
end.
Abort.
+
+Ltac f x y z :=
+ symmetry in x, y;
+ auto with z;
+ auto;
+ intros;
+ clearbody x;
+ generalize dependent z.
+
+Print Ltac f.
+
+(* Error messages *)
+
+Ltac g1 x := refine x.
+Tactic Notation "g2" constr(x) := g1 x.
+Tactic Notation "f1" constr(x) := refine x.
+Ltac f2 x := f1 x.
+Goal False.
+Fail g1 I.
+Fail f1 I.
+Fail g2 I.
+Fail f2 I.
+
+Ltac h x := injection x.
+Goal True -> False.
+Fail h I.
+intro H.
+Fail h H.
+
+(* Check printing of the "var" argument "Hx" *)
+Ltac m H := idtac H; exact H.
+Goal True.
+let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
+
+(* Check consistency of interpretation scopes (#4398) *)
+
+Goal nat*(0*0=0) -> nat*(0*0=0). intro.
+match goal with H: ?x*?y |- _ => idtac x end.
+match goal with |- ?x*?y => idtac x end.
+match goal with H: context [?x*?y] |- _ => idtac x end.
+match goal with |- context [?x*?y] => idtac x end.
+Abort.
diff --git a/test-suite/output/onlyprinting.out b/test-suite/output/onlyprinting.out
new file mode 100644
index 00000000..e0a30fcf
--- /dev/null
+++ b/test-suite/output/onlyprinting.out
@@ -0,0 +1,2 @@
+0:-) 0
+ : nat
diff --git a/test-suite/output/onlyprinting.v b/test-suite/output/onlyprinting.v
new file mode 100644
index 00000000..1973385a
--- /dev/null
+++ b/test-suite/output/onlyprinting.v
@@ -0,0 +1,5 @@
+Reserved Notation "x :-) y" (at level 50, only printing).
+
+Notation "x :-) y" := (plus x y).
+
+Check 0 + 0.
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
new file mode 100644
index 00000000..9300c3f5
--- /dev/null
+++ b/test-suite/output/qualification.out
@@ -0,0 +1,3 @@
+File "stdin", line 19, characters 0-7:
+Error: Signature components for label test do not match: expected type
+"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v
new file mode 100644
index 00000000..d39097e2
--- /dev/null
+++ b/test-suite/output/qualification.v
@@ -0,0 +1,19 @@
+Module Type T1.
+ Parameter t : Type.
+End T1.
+
+Module Type T2.
+ Declare Module M : T1.
+ Parameter t : Type.
+ Parameter test : t = M.t.
+End T2.
+
+Module M1 <: T1.
+ Definition t : Type := bool.
+End M1.
+
+Module M2 <: T2.
+ Module M := M1.
+ Definition t : Type := nat.
+ Lemma test : t = t. Proof. reflexivity. Qed.
+End M2.
diff --git a/test-suite/output/set.out b/test-suite/output/set.out
index 4dfd2bc2..4b72d73e 100644
--- a/test-suite/output/set.out
+++ b/test-suite/output/set.out
@@ -3,16 +3,16 @@
y1 := 0 : nat
x := 0 + 0 : nat
============================
- x = x
+ x = x
1 subgoal
y1, y2 := 0 : nat
x := y2 + 0 : nat
============================
- x = x
+ x = x
1 subgoal
y1, y2, y3 := 0 : nat
x := y2 + y3 : nat
============================
- x = x
+ x = x
diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out
index 73888da9..526e468f 100644
--- a/test-suite/output/simpl.out
+++ b/test-suite/output/simpl.out
@@ -2,14 +2,14 @@
x : nat
============================
- x = S x
+ x = S x
1 subgoal
x : nat
============================
- 0 + x = S x
+ 0 + x = S x
1 subgoal
x : nat
============================
- x = 1 + x
+ x = 1 + x
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
new file mode 100644
index 00000000..209b2bc2
--- /dev/null
+++ b/test-suite/output/subst.out
@@ -0,0 +1,97 @@
+1 subgoal
+
+ y, z : nat
+ Hy : y = 0
+ Hz : z = 0
+ H1 : 0 = 1
+ HA : True
+ H2 : 0 = 2
+ H3 : y = 3
+ HB : True
+ H4 : z = 4
+ ============================
+ True
+1 subgoal
+
+ x, z : nat
+ Hx : x = 0
+ Hz : z = 0
+ H1 : x = 1
+ HA : True
+ H2 : x = 2
+ H3 : 0 = 3
+ HB : True
+ H4 : z = 4
+ ============================
+ True
+1 subgoal
+
+ x, y : nat
+ Hx : x = 0
+ Hy : y = 0
+ H1 : x = 1
+ HA : True
+ H2 : x = 2
+ H3 : y = 3
+ HB : True
+ H4 : 0 = 4
+ ============================
+ True
+1 subgoal
+
+ H1 : 0 = 1
+ HA : True
+ H2 : 0 = 2
+ H3 : 0 = 3
+ HB : True
+ H4 : 0 = 4
+ ============================
+ True
+1 subgoal
+
+ y, z : nat
+ Hy : y = 0
+ Hz : z = 0
+ HA : True
+ H3 : y = 3
+ HB : True
+ H4 : z = 4
+ H1 : 0 = 1
+ H2 : 0 = 2
+ ============================
+ True
+1 subgoal
+
+ x, z : nat
+ Hx : x = 0
+ Hz : z = 0
+ H1 : x = 1
+ HA : True
+ H2 : x = 2
+ HB : True
+ H4 : z = 4
+ H3 : 0 = 3
+ ============================
+ True
+1 subgoal
+
+ x, y : nat
+ Hx : x = 0
+ Hy : y = 0
+ H1 : x = 1
+ HA : True
+ H2 : x = 2
+ H3 : y = 3
+ HB : True
+ H4 : 0 = 4
+ ============================
+ True
+1 subgoal
+
+ HA, HB : True
+ H4 : 0 = 4
+ H3 : 0 = 3
+ H1 : 0 = 1
+ H2 : 0 = 2
+ ============================
+ True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
new file mode 100644
index 00000000..e48aa6bb
--- /dev/null
+++ b/test-suite/output/subst.v
@@ -0,0 +1,48 @@
+(* Ensure order of hypotheses is respected after "subst" *)
+
+Set Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *)
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+Unset Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+
diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out
new file mode 100644
index 00000000..ae846036
--- /dev/null
+++ b/test-suite/output/unifconstraints.out
@@ -0,0 +1,65 @@
+3 focused subgoals
+(shelved: 1)
+
+ ============================
+ ?Goal 0
+
+subgoal 2 is:
+ forall n : nat, ?Goal n -> ?Goal (S n)
+subgoal 3 is:
+ nat
+unification constraint:
+ ?Goal ?Goal2 <=
+ True /\ True /\ True \/
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier
+3 focused subgoals
+(shelved: 1)
+
+ n, m : nat
+ ============================
+ ?Goal@{n:=n; m:=m} 0
+
+subgoal 2 is:
+ forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0)
+subgoal 3 is:
+ nat
+unification constraint:
+ ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
+ True /\ True /\ True \/
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier
+3 focused subgoals
+(shelved: 1)
+
+ m : nat
+ ============================
+ ?Goal1@{m:=m} 0
+
+subgoal 2 is:
+ forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0)
+subgoal 3 is:
+ nat
+unification constraint:
+
+ n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <=
+ True /\ True /\ True \/
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier
+3 focused subgoals
+(shelved: 1)
+
+ m : nat
+ ============================
+ ?Goal0@{m:=m} 0
+
+subgoal 2 is:
+ forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0)
+subgoal 3 is:
+ nat
+unification constraint:
+
+ n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <=
+ True /\ True /\ True \/
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
new file mode 100644
index 00000000..b9413a4a
--- /dev/null
+++ b/test-suite/output/unifconstraints.v
@@ -0,0 +1,22 @@
+(* Set Printing Existential Instances. *)
+Unset Solve Unification Constraints.
+Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
+Goal True /\ True /\ True \/
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier.
+ refine (nat_rect _ _ _ _).
+ Show.
+Admitted.
+
+Set Printing Existential Instances.
+Goal forall n m : nat, True /\ True /\ True \/
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+ veeryyyyyyyyyyyyloooooooooooooonggidentifier.
+ intros.
+ refine (nat_rect _ _ _ _).
+ Show.
+ clear n.
+ Show.
+ 3:clear m.
+ Show.
+Admitted.