11 files changed, 44 insertions, 7 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 34a1900bbc..37091a49e5 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -36,9 +36,10 @@ include ../Makefile.common
 # easily overridden
 LIB := ..
 BIN := $(shell cd ..; pwd)/bin/
+COQFLAGS?=
 
-coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite
-coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
+coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS)
+coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS)
 coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
 coqdoc := $(BIN)coqdoc
 coqtopbyte := $(BIN)coqtop.byte
diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v
new file mode 100644
index 0000000000..9816954d0c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8369.v
@@ -0,0 +1,3 @@
+(* Was failing in master with a not_found generated by the printer *)
+
+Fail Definition foo := fun '(u, v) p2 => (u, v).
diff --git a/test-suite/bugs/closed/bug_9240.v b/test-suite/bugs/closed/bug_9240.v
new file mode 100644
index 0000000000..e0901dc2d9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9240.v
@@ -0,0 +1,12 @@
+Register unit as core.IDProp.type.
+Register tt as core.IDProp.idProp.
+
+
+Inductive vec (A : Type) : nat -> Type :=
+| nil : vec A 0
+| cons : forall n : nat, A -> vec A n -> vec A (S n).
+
+Definition hd (A : Type) (n : nat) (v : vec A (S n)) : A :=
+match v in (vec _ (S n)) return A with
+| cons _ _ h _ => h
+end. (* assertion failure in evarconv *)
diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v
new file mode 100644
index 0000000000..a80f3233a3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9300.v
@@ -0,0 +1,6 @@
+Existing Class True.
+
+Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined.
+
+Fail Check foo (n := 3) true (s := (4 , 5)).
+Check foo (n := 3) (b := true) (4 , 5).
diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v
index e1c29a954c..baf87631f0 100644
--- a/test-suite/bugs/opened/bug_3166.v
+++ b/test-suite/bugs/opened/bug_3166.v
@@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True.
   compute in H0.
   change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
   Fail pose proof (fun k => @eq_trans _ _ _ k H0).
+Abort.
diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v
index a717bbe735..18820b1a4c 100644
--- a/test-suite/bugs/opened/bug_3754.v
+++ b/test-suite/bugs/opened/bug_3754.v
@@ -282,3 +282,4 @@ Defined.
       rewrite <- ap_p_pp; rewrite_moveL_Mp_p.
       Set Debug Tactic Unification.
       Fail rewrite (concat_Ap ff2).
+    Abort.
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
index 5c74addb62..78b2aa69b9 100644
--- a/test-suite/bugs/opened/bug_3890.v
+++ b/test-suite/bugs/opened/bug_3890.v
@@ -1,3 +1,5 @@
+Set Nested Proofs Allowed.
+
 Class Foo.
 Class Bar := b : Type.
 
diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v
index 2d0d1930f1..3c7c945ed8 100644
--- a/test-suite/bugs/opened/bug_3938.v
+++ b/test-suite/bugs/opened/bug_3938.v
@@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b.
   intros a b f H.
   rewrite H. (* Toplevel input, characters 15-25:
 Anomaly: Evar ?X11 was not declared. Please report. *)
+Abort.
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
index ae5d51bae8..b7c98aa134 100644
--- a/test-suite/output-modulo-time/ltacprof_cutoff.v
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-profile-ltac") -*- *)
+(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *)
 Require Coq.ZArith.BinInt.
 Module WithIdTac.
   Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index cf2d5b2850..14c48e8fa0 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -9,10 +9,11 @@ The command has indeed failed with message:
 Ltac call to "instantiate ( (ident) := (lglob) )" failed.
 Instance is not well-typed in the environment of ?x.
 The command has indeed failed with message:
-Cannot infer the domain of the type of f.
+Cannot infer ?T in the partial instance "?T -> nat" found for the type of f.
 The command has indeed failed with message:
-Cannot infer the domain of the implicit parameter A of id whose type is
-"Type".
+Cannot infer ?T in the partial instance "?T -> nat" found for the implicit
+parameter A of id whose type is "Type".
 The command has indeed failed with message:
-Cannot infer the codomain of the type of f in environment:
+Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the
+type of f in environment:
 x : nat
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 52fe98ac07..232ac17cbf 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1873,3 +1873,12 @@ Check match niln in listn O return O=O with niln => eq_refl end.
 (* (was failing up to May 2017) *)
 
 Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end.
+
+(* A test about binding variables of "in" clause of "match" *)
+(* (was failing from 8.5 to Dec 2018) *)
+
+Check match O in nat return nat with O => O | _ => O end.
+
+(* Checking that aliases are substituted in the correct order *)
+
+Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0.