20 files changed, 217 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index c10cd4ed44..e87e133768 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -44,7 +44,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1)
 
 # read out an emacs config and look for coq-prog-args; if such exists, return it
 get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1)
-get_coq_prog_args = $(strip $(filter-out "-emacs-U" "-emacs",$(shell $(call get_coq_prog_args_helper,$(1)))))
+get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1))))
 SINGLE_QUOTE="
 #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter
 # wrap the arguments in parens, but only if they exist
diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v
new file mode 100644
index 0000000000..806ffb771f
--- /dev/null
+++ b/test-suite/bugs/closed/4132.v
@@ -0,0 +1,31 @@
+
+Require Import ZArith Omega.
+Open Scope Z_scope.
+
+(** bug 4132: omega was using "simpl" either on whole equations, or on
+   delimited but wrong spots. This was leading to unexpected reductions
+   when one atom (here [b]) is an evaluable reference instead of a variable. *)
+
+Lemma foo
+  (x y x' zxy zxy' z : Z)
+  (b := 5)
+  (Ry : - b <= y < b)
+  (Bx : x' <= b)
+  (H : - zxy' <= zxy)
+  (H' : zxy' <= x') : - b <= zxy.
+Proof.
+omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
+Qed.
+
+Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
+omega. (* Pierre L: according to a comment of bug report #4132,
+          this might have triggered "index out of bounds" in the past,
+          but I never managed to reproduce that in any version,
+          even before my fix. *)
+Qed.
+
+Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
+omega. (* Pierre L: according to a comment of bug report #4132,
+          this might have triggered "Failure(occurence 2)" in the past,
+          but I never managed to reproduce that. *)
+Qed.
diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v
new file mode 100644
index 0000000000..390133162f
--- /dev/null
+++ b/test-suite/bugs/closed/5486.v
@@ -0,0 +1,15 @@
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k :
+									 forall _ : T, Fm),
+    @eq Fm
+	(k
+	   match p return T with
+	   | pair p0 swap => fst p0
+	   end) f.
+  intros.
+  (* next statement failed in Bug 5486 *)
+  match goal with
+  | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ]
+    => pose (let (a, b) := d in e a b) as t0
+  end.
diff --git a/test-suite/bugs/closed/5522.v b/test-suite/bugs/closed/5522.v
new file mode 100644
index 0000000000..0fae9ede42
--- /dev/null
+++ b/test-suite/bugs/closed/5522.v
@@ -0,0 +1,7 @@
+(* Checking support for scope delimiters and as clauses in 'pat
+   applied to notations with binders *)
+
+Notation "'multifun' x .. y 'in' f" := (fun x => .. (fun y => f) .. )
+  (at level 200, x binder, y binder, f at level 200).
+
+Check multifun '((x, y)%core as z) in (x+y,0)=z.
diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v
new file mode 100644
index 0000000000..88f219be30
--- /dev/null
+++ b/test-suite/bugs/closed/5526.v
@@ -0,0 +1,3 @@
+Fail Notation "x === x" := (eq_refl x) (at level 10).
+Reserved Notation "x === x" (only printing, at level 10).
+Notation "x === x" := (eq_refl x) (only printing).
diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v
new file mode 100644
index 0000000000..bb1222489a
--- /dev/null
+++ b/test-suite/bugs/closed/5550.v
@@ -0,0 +1,10 @@
+Section foo.
+
+  Variable bar : Prop.
+  Variable H : bar.
+
+  Goal bar.
+    typeclasses eauto with foobar.
+  Qed.
+
+End foo.
diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v
index 84a4009d7e..19eea94b19 100644
--- a/test-suite/coqchk/univ.v
+++ b/test-suite/coqchk/univ.v
@@ -33,3 +33,16 @@ Inductive finite_of_order T (D : T -> Type) (n : natural) :=
     (rank_injective : injective_in T natural D rank)
     (rank_onto :
        forall i, equivalent (less_than i n) (in_image T natural D rank i)).
+
+(* Constraints *)
+Universes i j.
+Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})).
+Constraint i < j.
+Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}).
+Universes i' j'.
+Constraint i' = j'.
+Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})).
+Inductive constraint4 : (Type -> Type) -> Type
+  := mk_constraint4 : let U1 := Type in
+                      let U2 := Type in
+                      constraint4 (fun x : U1 => (x : U2)).
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 8ce6f9795c..f064dfe763 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -2,18 +2,18 @@ t_rect =
 fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
-  | @k _ x0 => f x0 (F x0)
+  | k _ x0 => f x0 (F x0)
   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
+                     | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
      = fun d : TT => match d with
-                     | @CTT _ _ b => b
+                     | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
 proj = 
@@ -72,3 +72,11 @@ e1 : texp t1
 e2 : texp t2
 The term "0" has type "nat" while it is expected to have type
  "typeDenote t0".
+fun '{{n, m, _}} => n + m
+     : J -> nat
+fun '{{n, m, p}} => n + m + p
+     : J -> nat
+fun '(D n m p q) => n + m + p + q
+     : J -> nat
+The command has indeed failed with message:
+The constructor D (in type J) expects 3 arguments.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4074896420..6a4fd007df 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -106,3 +106,18 @@ Fail Fixpoint texpDenote t (e:texp t):typeDenote t:=
   | TBinop t1 t2 _ b e1 e2 => O
   end.
 
+(* Test notations with local definitions in constructors *)
+
+Inductive J := D : forall n m, let p := n+m in nat -> J.
+Notation "{{ n , m , q }}" := (D n m q).
+
+Check fun x : J => let '{{n, m, _}} := x in n + m.
+Check fun x : J => let '{{n, m, p}} := x in n + m + p.
+
+(* Cannot use the notation because of the dependency in p *)
+
+Check fun x => let '(D n m p q) := x in n+m+p+q.
+
+(* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
+
+Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 360f379676..0cb870c577 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -98,3 +98,7 @@ 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
+fun x : ?A => x === x
+     : forall x : ?A, x = x
+where
+?A : [x : ?A |- Type] (x cannot be used)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 4b8bfe3124..5676fe8c7c 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -139,3 +139,9 @@ Notation "'tele' x .. z := b" :=
   (at level 85, x binder, z binder).
 
 Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
+
+(**********************************************************************)
+(* Test printing of #5526                                             *)
+
+Notation "x === x" := (eq_refl x) (only printing, at level 10).
+Check (fun x => eq_refl x).
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index 36d643a447..d45343fe60 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -14,3 +14,19 @@ build 5
      : test_r
 build_c 5
      : test_c
+fun '(C _ p) => p
+     : N -> True
+fun '{| T := T |} => T
+     : N -> Type
+fun '(C T p) => (T, p)
+     : N -> Type * True
+fun '{| q := p |} => p
+     : M -> True
+fun '{| U := T |} => T
+     : M -> Type
+fun '{| U := T; q := p |} => (T, p)
+     : M -> Type * True
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+     : M -> Type * True * nat
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+     : M -> Type * True * nat
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 6aa3df9830..d9a649fadc 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -19,3 +19,15 @@ Check build 5.
 Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
+
+Record N := C { T : Type; _ : True }.
+Check fun x:N => let 'C _ p := x in p.
+Check fun x:N => let 'C T _ := x in T.
+Check fun x:N => let 'C T p := x in (T,p).
+
+Record M := D { U : Type; a := 0; q : True }.
+Check fun x:M => let 'D T _ p := x in p.
+Check fun x:M => let 'D T _ p := x in T.
+Check fun x:M => let 'D T p := x in (T,p).
+Check fun x:M => let 'D T a p := x in (T,p,a).
+Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a).
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
new file mode 100644
index 0000000000..d0c963be17
--- /dev/null
+++ b/test-suite/output/Show.out
@@ -0,0 +1,12 @@
+3 subgoals, subgoal 1 (ID 29)
+  
+  H : 0 = 0
+  ============================
+  1 = 1
+
+subgoal 2 (ID 33) is:
+ 1 = S (S m')
+subgoal 3 (ID 20) is:
+ S (S n') = S m
+(dependent evars: (printing disabled) )
+
diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v
new file mode 100644
index 0000000000..60faac8dd9
--- /dev/null
+++ b/test-suite/output/Show.v
@@ -0,0 +1,11 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *)
+
+(* tests of Show output with -emacs flag to coqtop; see bug 5535 *)
+
+Theorem nums : forall (n m : nat), n = m -> (S n) = (S m).
+Proof.
+  intros.
+  induction n as [| n'].  
+  induction m as [| m'].
+  Show.
+Admitted.
diff --git a/test-suite/output/ShowMatch.out b/test-suite/output/ShowMatch.out
new file mode 100644
index 0000000000..e5520b8dfa
--- /dev/null
+++ b/test-suite/output/ShowMatch.out
@@ -0,0 +1,8 @@
+match # with
+ | f =>
+ end
+ 
+match # with
+ | A.f =>
+ end
+ 
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v
new file mode 100644
index 0000000000..02b7eada83
--- /dev/null
+++ b/test-suite/output/ShowMatch.v
@@ -0,0 +1,13 @@
+(* Bug 5546 complained about unqualified constructors in Show Match output, 
+   when qualification is needed to disambiguate them
+*)
+
+Module A.
+  Inductive foo := f.
+  Show Match foo. (* no need to disambiguate *)
+End A. 
+
+Module B.
+  Inductive foo := f.
+  (* local foo shadows A.foo, so constructor "f" needs disambiguation *)
+  Show Match A.foo. 
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 49c465b6c6..52fe98ac07 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1868,3 +1868,8 @@ Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
 Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.
 
 Check match niln in listn O return O=O with niln => eq_refl end.
+
+(* A test about nested "as" clauses *)
+(* (was failing up to May 2017) *)
+
+Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end.
diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v
new file mode 100644
index 0000000000..6aeb05f54e
--- /dev/null
+++ b/test-suite/success/cbn.v
@@ -0,0 +1,18 @@
+(* cbn is able to refold mutual recursive calls *)
+
+Fixpoint foo (n : nat) :=
+  match n with
+  | 0 => true
+  | S n => g n
+  end
+with g (n : nat) : bool :=
+  match n with
+  | 0 => true
+  | S n => foo n
+  end.
+Goal forall n, foo (S n) = g n.
+  intros. cbn.
+  match goal with
+    |- g _ = g _ => reflexivity
+  end.
+Qed.
+\ No newline at end of file
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 4e2bf45118..4b2f7b53e1 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -414,4 +414,10 @@ Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2.
 Import EqNotations.
 Definition test2 {A B:Type} {H:A=B} (a:A) : B := rew H in a.
 
+(* Check that pre-existing evars are not counted as newly undefined in "set" *)
+(* Reported by Théo *)
 
+Goal exists n : nat, n = n -> True.
+eexists.
+set (H := _ = _).
+Abort.