10 files changed, 85 insertions, 9 deletions
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
new file mode 100644
index 00000000..e912003f
--- /dev/null
+++ b/test-suite/output/Inductive.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Last occurrence of "list'" must have "A" as 1st argument in
+ "A -> list' A -> list' (A * A)%type".
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
new file mode 100644
index 00000000..8db8956e
--- /dev/null
+++ b/test-suite/output/Inductive.v
@@ -0,0 +1,3 @@
+Fail Inductive list' (A:Set) : Set :=
+| nil' : list' A
+| cons' : A -> list' A -> list' (A*A).
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 6efd671a..b1558dab 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -70,7 +70,7 @@ FST (0; 1)
      : Z
 Nil
      : forall A : Type, list A
-NIL:list nat
+NIL : list nat
      : list nat
 (false && I 3)%bool /\ I 6
      : Prop
@@ -78,7 +78,7 @@ NIL:list nat
      : Z * Z * Z * (Z * Z * Z)
 [|0 * (1, 2, 3); (4, 5, 6) * false|]
      : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
-fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
+fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z
      : (Z -> Z -> Z -> Z) -> Z
 Init.Nat.add
      : nat -> nat -> nat
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 08df9150..66458543 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -2,11 +2,6 @@ Axioms:
 foo : nat
 Axioms:
 foo : nat
-Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZAdd
-Fetching opaque proofs from disk for Coq.Arith.PeanoNat
-Fetching opaque proofs from disk for Coq.Classes.Morphisms
-Fetching opaque proofs from disk for Coq.Init.Logic
-Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZBase
 Axioms:
 extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
@@ -21,3 +16,5 @@ extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
 Closed under the global context
 Closed under the global context
+Axioms:
+M.foo : False
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index f23bc498..c2003816 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -94,3 +94,19 @@ Proof (false_positive.add_comm 5).
 
 Print Assumptions comm_plus5.
 (* Should answer : Closed under the global context *)
+
+(** Print Assumption and Include *)
+
+Module INCLUDE.
+
+Module M.
+Axiom foo : False.
+End M.
+
+Module N.
+Include M.
+End N.
+
+Print Assumptions N.foo.
+
+End INCLUDE.
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
new file mode 100644
index 00000000..db464fd0
--- /dev/null
+++ b/test-suite/output/PrintModule.out
@@ -0,0 +1,4 @@
+Module N : S with Definition T := nat := M
+
+Module N : S with Module T := K := M
+
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
new file mode 100644
index 00000000..999d9a98
--- /dev/null
+++ b/test-suite/output/PrintModule.v
@@ -0,0 +1,34 @@
+Module FOO.
+
+Module M.
+ Definition T := nat.
+End M.
+
+Module Type S.
+ Parameter T : Set.
+End S.
+
+Module N : S with Definition T := nat := M.
+
+Print Module N.
+
+End FOO.
+
+Module BAR.
+
+Module K. End K.
+Module Type KS. End KS.
+
+Module M.
+ Module T := K.
+End M.
+
+Module Type S.
+ Declare Module T : KS.
+End S.
+
+Module N : S with Module T := K := M.
+
+Print Module N.
+
+End BAR.
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index b1952aec..f2d14477 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,12 +6,12 @@ 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 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] 
-fun n : nat => ?y ?y0:T n
+fun n : nat => ?y ?y0 : T n
      : forall n : nat, T n
 where
 ?y : [n : nat |- ?T0 -> T n] 
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
new file mode 100644
index 00000000..d003c70d
--- /dev/null
+++ b/test-suite/output/ltac.out
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
new file mode 100644
index 00000000..7e2610c7
--- /dev/null
+++ b/test-suite/output/ltac.v
@@ -0,0 +1,17 @@
+(* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
+Goal True.
+Fail let T := constr:((fun a b : nat => a+b) 1 1) in
+  lazymatch T with
+  | (fun x z => ?y) 1 1
+    => pose ((fun x _ => y) 1 1)
+  end.
+Abort.
+
+(* This should not raise a warning (see #4317) *)
+Goal True.
+assert (H:= eq_refl ((fun x => x) 1)).
+let HT := type of H in
+lazymatch goal with
+| H1 : HT |- _ => idtac
+end.
+Abort.