11 files changed, 63 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4957.v b/test-suite/bugs/closed/4957.v
new file mode 100644
index 0000000000..0efd87ac0d
--- /dev/null
+++ b/test-suite/bugs/closed/4957.v
@@ -0,0 +1,6 @@
+Ltac get_value H := eval cbv delta [H] in H.
+
+Goal True.
+refine (let X := _ in _).
+let e := get_value X in unify e Prop.
+Abort.
diff --git a/test-suite/bugs/closed/5435.v b/test-suite/bugs/closed/5435.v
new file mode 100644
index 0000000000..60ace5ce96
--- /dev/null
+++ b/test-suite/bugs/closed/5435.v
@@ -0,0 +1,2 @@
+Definition foo (x : nat) := Eval native_compute in x.
+
diff --git a/test-suite/bugs/closed/5460.v b/test-suite/bugs/closed/5460.v
new file mode 100644
index 0000000000..50221cdd83
--- /dev/null
+++ b/test-suite/bugs/closed/5460.v
@@ -0,0 +1,11 @@
+(* Bugs in computing dependencies in pattern-matching compilation *)
+
+Inductive A := a1 | a2.
+Inductive B := b.
+Inductive C : A -> Type := c : C a1 | d : C a2.
+Definition P (x : A) (y : C x) (z : B) : nat :=
+  match z, x, y with
+      | b, a1, c => 0
+      | b, a2, d => 0
+      | _, _, _ => 1
+  end.
diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out
new file mode 100644
index 0000000000..851ecd9306
--- /dev/null
+++ b/test-suite/output/ErrorInModule.out
@@ -0,0 +1,2 @@
+File "stdin", line 3, characters 20-31:
+Error: The reference nonexistent was not found in the current environment.
diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v
new file mode 100644
index 0000000000..e69e23276b
--- /dev/null
+++ b/test-suite/output/ErrorInModule.v
@@ -0,0 +1,4 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+Module M.
+  Definition foo := nonexistent.
+End M.
diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out
new file mode 100644
index 0000000000..851ecd9306
--- /dev/null
+++ b/test-suite/output/ErrorInSection.out
@@ -0,0 +1,2 @@
+File "stdin", line 3, characters 20-31:
+Error: The reference nonexistent was not found in the current environment.
diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v
new file mode 100644
index 0000000000..3036f8f05b
--- /dev/null
+++ b/test-suite/output/ErrorInSection.v
@@ -0,0 +1,4 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *)
+Section S.
+  Definition foo := nonexistent.
+End S.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
new file mode 100644
index 0000000000..128bc77673
--- /dev/null
+++ b/test-suite/output/UnivBinders.out
@@ -0,0 +1,6 @@
+bar@{u} = nat
+     : Wrap@{u} Set
+(* u |= Set < u
+         *)
+
+bar is universe polymorphic
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
new file mode 100644
index 0000000000..d9e89e43c6
--- /dev/null
+++ b/test-suite/output/UnivBinders.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Class Wrap A := wrap : A.
+
+Instance bar@{u} : Wrap@{u} Set. Proof nat.
+Print bar.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 52acad7460..837f2efd06 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -121,6 +121,7 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
 Goal True.
 {{ exact I. }}
 Qed.
+
 Check |- {{ 0 }} 0.
 
 (* Check parsing of { and } is not affected by notations #3479 *)
@@ -135,3 +136,9 @@ Notation "" := (@nil) (only printing).
 
 (* Check that a notation cannot be neither parsing nor printing. *)
 Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
+
+(* Check "where" clause for inductive types with parameters *)
+
+Reserved Notation "x === y" (at level 50).
+Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
+ where "x === y" := (EQ x y).
diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v
index 048b53d26c..fe3b8c1d7c 100644
--- a/test-suite/success/univnames.v
+++ b/test-suite/success/univnames.v
@@ -21,6 +21,17 @@ Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla.
 Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy.
 
 
+Class Wrap A := wrap : A.
+
+Fail Instance bad@{} : Wrap Type := Type.
+
+Instance bad@{} : Wrap Type.
+Fail Proof Type.
+Abort.
+
+Instance bar@{u} : Wrap@{u} Set. Proof nat.
+
+
 Monomorphic Universe g.
 
-Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
-\ No newline at end of file
+Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.