16 files changed, 177 insertions, 37 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 2c7b04c62a..a2ee2d4c8e 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 05eeaac631..bd9240476f 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/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 3488cb3056..9d90de47cb 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,9 +1,12 @@
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
+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
@@ -101,15 +104,16 @@ 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: Arguments lists should agree on 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.
 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.
+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 b6fbeb6ec7..2d14c94ac8 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,5 +1,5 @@
 Fail Arguments eq_refl {B y}, [B] y.
-Fail Arguments identity T _ _.
+Arguments identity A _ _.
 Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
@@ -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] : rename.
 Fail Arguments eq_refl {F F}, [F] F.
-Fail Arguments eq {F} x [z].
+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/Cases.out b/test-suite/output/Cases.out
index 2b828d382a..8ce6f9795c 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -56,3 +56,19 @@ match H with
      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 3c2eaf42c9..4074896420 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -77,3 +77,32 @@ 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/Notations2.out b/test-suite/output/Notations2.out
index 5541ccf57b..ad60aeccce 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -60,3 +60,27 @@ exist (Q x) y conj
      : 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 1d8278c088..ceb29d1b9e 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -116,3 +116,32 @@ Check %j.
 
 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/PrintModule.out b/test-suite/output/PrintModule.out
index db464fd07e..751d5fcc48 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 999d9a9862..5f30f7cda6 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/SearchPattern.out b/test-suite/output/SearchPattern.out
index 1eb7eca8f1..f3c12effca 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/ltac.out b/test-suite/output/ltac.out
index f4254e4e2f..a7bde5ea3f 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -26,3 +26,8 @@ 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 dfa60eeda0..76c37625aa 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -43,3 +43,17 @@ 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/qualification.out b/test-suite/output/qualification.out
new file mode 100644
index 0000000000..9300c3f546
--- /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 0000000000..d39097e2dd
--- /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/unifconstraints.out b/test-suite/output/unifconstraints.out
index d152052ba3..ae84603622 100644
--- a/test-suite/output/unifconstraints.out
+++ b/test-suite/output/unifconstraints.out
@@ -8,11 +8,7 @@ subgoal 2 is:
  forall n : nat, ?Goal n -> ?Goal (S n)
 subgoal 3 is:
  nat
-unification constraints:
- ?Goal ?Goal2 <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  ?Goal ?Goal2 <=
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
@@ -28,11 +24,7 @@ subgoal 2 is:
  forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0)
 subgoal 3 is:
  nat
-unification constraints:
- ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
@@ -48,12 +40,7 @@ subgoal 2 is:
  forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0)
 subgoal 3 is:
  nat
-unification constraints:
- 
- n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  
  n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <=
    True /\ True /\ True \/
@@ -70,12 +57,7 @@ subgoal 2 is:
  forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0)
 subgoal 3 is:
  nat
-unification constraints:
- 
- n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  
  n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <=
    True /\ True /\ True \/