18 files changed, 102 insertions, 27 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_2830.v b/test-suite/bugs/closed/bug_2830.v
index 801c61b132..a321bb324e 100644
--- a/test-suite/bugs/closed/bug_2830.v
+++ b/test-suite/bugs/closed/bug_2830.v
@@ -194,14 +194,17 @@ Instance skel_equiv A : Equivalence (@skel A).
 Admitted.
 
 Import FunctionalExtensionality.
-Instance set_cat : Category Type (fun A B => A -> B) := {
+
+Instance set_cat : Category Type (fun A B => A -> B).
+refine {|
   id := fun A => fun x => x
   ; comp c b a f g := fun x => f (g x)
   ; eqv := fun A B => @skel (A -> B)
-}.
+|}.
 intros. compute. symmetry. apply eta_expansion.
 intros. compute. symmetry. apply eta_expansion.
-intros. compute. reflexivity. Defined.
+intros. compute. reflexivity.
+Defined.
 
 (* The [list] type constructor is a Functor. *)
 
diff --git a/test-suite/bugs/closed/bug_3495.v b/test-suite/bugs/closed/bug_3495.v
index 7b0883f910..47db64a096 100644
--- a/test-suite/bugs/closed/bug_3495.v
+++ b/test-suite/bugs/closed/bug_3495.v
@@ -1,7 +1,7 @@
 Require Import RelationClasses.
 
 Axiom R : Prop -> Prop -> Prop.
-Declare Instance : Reflexive R.
+Declare Instance R_refl : Reflexive R.
 
 Class bar := { x : False }.
 Record foo := { a : Prop ; b : bar }.
diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v
index 379e46b3e3..9b3210860c 100644
--- a/test-suite/bugs/closed/bug_4498.v
+++ b/test-suite/bugs/closed/bug_4498.v
@@ -19,6 +19,6 @@ Class Category := {
 
 Require Export Coq.Setoids.Setoid.
 
-Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with
   signature equiv ==> equiv ==> equiv as compose_mor.
 Proof. apply comp_respects. Qed.
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/closed/bug_9329.v b/test-suite/bugs/closed/bug_9329.v
new file mode 100644
index 0000000000..c0322dec40
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9329.v
@@ -0,0 +1,12 @@
+(* Declare empty levels in the same order they are computed *)
+
+Notation "< a ; b ; c >1" :=
+  (sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21).
+Notation "< a ; b ; c >2" :=
+  (sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31).
+Notation "< a ; b ; c >3" :=
+  (sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41).
+Notation "< a ; b ; c >4" :=
+  (sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49).
+Notation "< a ; b >" :=
+  (sum a b) (at level 61, a at level 63, b at level 62).
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..9d83743b2a 100644
--- a/test-suite/bugs/opened/bug_3890.v
+++ b/test-suite/bugs/opened/bug_3890.v
@@ -1,7 +1,11 @@
+Set Nested Proofs Allowed.
+
 Class Foo.
 Class Bar := b : Type.
 
+Set Refine Instance Mode.
 Instance foo : Foo := _.
+Unset Refine Instance Mode.
 (* 1 subgoals, subgoal 1 (ID 4)
 
   ============================
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.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 400479ae85..9086621344 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -198,7 +198,9 @@ Module UniqueInstances.
       for it. *)
   Set Typeclasses Unique Instances.
   Class Eq (A : Type) : Set.
+    Set Refine Instance Mode.
     Instance eqa : Eq nat := _. constructor. Qed.
+    Unset Refine Instance Mode.
     Instance eqb : Eq nat := {}.
     Class Foo (A : Type) (e : Eq A) : Set.
     Instance fooa : Foo _ eqa := {}.
diff --git a/test-suite/unit-tests/lib/pp_big_vect.ml b/test-suite/unit-tests/lib/pp_big_vect.ml
new file mode 100644
index 0000000000..e1cdd290e2
--- /dev/null
+++ b/test-suite/unit-tests/lib/pp_big_vect.ml
@@ -0,0 +1,14 @@
+open OUnit
+open Pp
+
+let pr_big_vect =
+  let n = "pr_big_vect" in
+  n >:: (fun () ->
+      let v = Array.make (1 lsl 20) () in
+      let pp = prvecti_with_sep spc (fun _ _ -> str"x") v in
+      let str = string_of_ppcmds pp in
+      ignore(str))
+
+let tests = [pr_big_vect]
+
+let () = Utest.run_tests __FILE__ (Utest.open_log_out_ch __FILE__) tests
diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
index 7f9e6cc6e0..d0b8d21b69 100644
--- a/test-suite/unit-tests/printing/proof_diffs_test.ml
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -51,23 +51,28 @@ let t () =
   assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed
 let _ = add_test "diff_str add/remove" t
 
-(* example of a limitation, not really a test *)
-let t () =
-  try
-    let _ = diff_str "a" "&gt;" in
-    assert_failure "unlexable string gives an exception"
-  with _ -> ()
-let _ = add_test "diff_str unlexable" t
-
-(* problematic examples for tokenize_string:
-   comments omitted
-   quoted string loses quote marks (are escapes supported/handled?)
-   char constant split into 2
+(* lexer tweaks:
+   comments are lexed as multiple tokens
+   strings tokens include begin/end quotes and embedded ""
+   single multibyte characters returned even if they're not keywords
+
+   inputs that give a lexer failure (but no use case needs them yet):
+     ".12"
+     unterminated string
+     invalid UTF-8 sequences
    *)
 let t () =
-  List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx");
-  cprintf "\n"
-let _ = add_test "tokenize_string examples" t
+  let str = "(* comment.field *) ?id () \"str\"\"ing\" \\ := Ж &gt; ∃ 'c' xx" in
+  let toks = tokenize_string str in
+  (*List.iter (fun x -> cprintf "'%s' " x) toks;*)
+  (*cprintf "\n";*)
+  let str_no_white = String.concat "" (String.split_on_char ' ' str) in
+  assert_equal ~printer:(fun x -> x) str_no_white (String.concat "" toks);
+  List.iter (fun s ->
+    assert_equal ~msg:("'" ^ s ^ "' is a single token") ~printer:string_of_bool true (List.mem s toks))
+    [ "(*"; "()"; ":="]
+
+let _ = add_test "tokenize_string/diff_mode in lexer" t
 
 open Pp