12 files changed, 113 insertions, 5 deletions
diff --git a/test-suite/bugs/2428.v b/test-suite/bugs/closed/2428.v
index a4f587a58d..b398a76d91 100644
--- a/test-suite/bugs/2428.v
+++ b/test-suite/bugs/closed/2428.v
@@ -5,6 +5,6 @@ Definition myFact := forall x, P x.
 Hint Extern 1 (P _) => progress (unfold myFact in *).
 
 Lemma test : (True -> myFact) -> P 3.
-Proof. 
+Proof.
   intros. debug eauto.
 Qed.
diff --git a/test-suite/bugs/closed/2670.v b/test-suite/bugs/closed/2670.v
index c401420e94..791889b24b 100644
--- a/test-suite/bugs/closed/2670.v
+++ b/test-suite/bugs/closed/2670.v
@@ -15,6 +15,14 @@ Proof.
   refine (match e return _ with refl_equal => _ end).
   reflexivity.
   Undo 2.
+  (** Check insensitivity to alphabetic order *)
+  refine (match e as a in _ = b return _ with refl_equal => _ end).
+  reflexivity.
+  Undo 2.
+  (** Check insensitivity to alphabetic order *)
+  refine (match e as z in _ = y return _ with refl_equal => _ end).
+  reflexivity.
+  Undo 2.
   (* Next line similarly has a dependent and a non dependent solution *)
   refine (match e with refl_equal => _ end).
   reflexivity.
diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/closed/4623.v
index 7ecfd98b67..7ecfd98b67 100644
--- a/test-suite/bugs/4623.v
+++ b/test-suite/bugs/closed/4623.v
diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/closed/4624.v
index f5ce981cd0..f5ce981cd0 100644
--- a/test-suite/bugs/4624.v
+++ b/test-suite/bugs/closed/4624.v
diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v
index 1507fa4bf0..bd9bac37ef 100644
--- a/test-suite/bugs/closed/4717.v
+++ b/test-suite/bugs/closed/4717.v
@@ -19,8 +19,6 @@ Proof.
   omega.
 Qed.
 
-Require Import ZArith ROmega.
-
 Open Scope Z_scope.
 
 Definition Z' := Z.
@@ -32,6 +30,4 @@ Theorem Zle_not_eq_lt : forall n m,
 Proof.
   intros.
   omega.
-  Undo.
-  romega.
 Qed.
diff --git a/test-suite/bugs/7333.v b/test-suite/bugs/closed/7333.v
index fba5b9029d..fba5b9029d 100644
--- a/test-suite/bugs/7333.v
+++ b/test-suite/bugs/closed/7333.v
diff --git a/test-suite/bugs/closed/7754.v b/test-suite/bugs/closed/7754.v
new file mode 100644
index 0000000000..229df93773
--- /dev/null
+++ b/test-suite/bugs/closed/7754.v
@@ -0,0 +1,21 @@
+
+Set Universe Polymorphism.
+
+Module OK.
+
+  Inductive one@{i j} : Type@{i} :=
+  with two : Type@{j} := .
+  Check one@{Set Type} : Set.
+  Fail Check two@{Set Type} : Set.
+
+End OK.
+
+Module Bad.
+
+  Fail Inductive one :=
+    with two@{i +} : Type@{i} := .
+
+  Fail Inductive one@{i +} :=
+    with two@{i +} := .
+
+End Bad.
diff --git a/test-suite/bugs/closed/8215.v b/test-suite/bugs/closed/8215.v
new file mode 100644
index 0000000000..c4b29a6354
--- /dev/null
+++ b/test-suite/bugs/closed/8215.v
@@ -0,0 +1,14 @@
+(* Check that instances for local definitions in evars have compatible body *)
+Goal False.
+Proof.
+  pose (n := 1).
+  evar (m:nat).
+  subst n.
+  pose (n := 0).
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clearbody n.
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clear n.
+  pose (n := 0+1).
+  Check ?m. (* Should be ok *)
+Abort.
diff --git a/test-suite/bugs/closed/8270.v b/test-suite/bugs/closed/8270.v
new file mode 100644
index 0000000000..f36f757f10
--- /dev/null
+++ b/test-suite/bugs/closed/8270.v
@@ -0,0 +1,15 @@
+(* Don't do zeta in cbn when not asked for *)
+
+Goal let x := 0 in
+     let y := x in
+     y = 0.
+  (* We use "cofix" as an example because there are obviously no
+     cofixpoints in sight.  This problem arises with any set of
+     reduction flags (not including zeta where the lets are of course reduced away) *)
+  cbn cofix.
+  intro x.
+  unfold x at 1. (* Should succeed *)
+  Undo 2.
+  cbn zeta.
+  Fail unfold x at 1.
+Abort.
diff --git a/test-suite/bugs/closed/8288.v b/test-suite/bugs/closed/8288.v
new file mode 100644
index 0000000000..0350be9c06
--- /dev/null
+++ b/test-suite/bugs/closed/8288.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Set Polymorphic Inductive Cumulativity.
+
+Inductive foo := C : (forall A : Type -> Type, A Type) -> foo.
+(* anomaly invalid subtyping relation *)
diff --git a/test-suite/bugs/closed/8432.v b/test-suite/bugs/closed/8432.v
new file mode 100644
index 0000000000..844ee12668
--- /dev/null
+++ b/test-suite/bugs/closed/8432.v
@@ -0,0 +1,39 @@
+Require Import Program.Tactics.
+
+Obligation Tactic := idtac.
+Set Universe Polymorphism.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Inductive Empty : Type :=.
+Inductive Unit : Type := tt.
+Definition not (A : Type) := A -> Empty.
+
+  Lemma nat_path_O_S (n : nat) (H : paths O (S n)) : Empty.
+  Proof. refine (
+    match H in paths _ i return
+      match i with
+      | O => Unit
+      | S _ => Empty
+      end
+    with
+    | idpath _ => tt
+    end
+  ). Defined.
+  Lemma symmetry {A} (x y : A) (p : paths x y) : paths y x.
+  Proof.
+    destruct p. apply idpath.
+  Defined.
+  Lemma nat_path_S_O (n : nat) (H : paths (S n) O) : Empty.
+  Proof. eapply nat_path_O_S. exact (symmetry _ _ H). Defined.
+Set Printing Universes.
+Program Fixpoint succ_not_zero (n:nat) : not (paths (S n) 0) :=
+match n as n return not (paths (S n) 0) with
+| 0 => nat_path_S_O _
+| S n' => let dummy := succ_not_zero n' in _
+end.
+Next Obligation.
+  intros f _ n dummy H. exact (nat_path_S_O _ H).
+  Show Universes.
+Defined.
diff --git a/test-suite/bugs/closed/8532.v b/test-suite/bugs/closed/8532.v
new file mode 100644
index 0000000000..00aa66e701
--- /dev/null
+++ b/test-suite/bugs/closed/8532.v
@@ -0,0 +1,8 @@
+(* Checking Print Assumptions relatively to a bound module *)
+
+Module Type Typ.
+  Parameter Inline(10) t : Type.
+End Typ.
+Module  Terms_mod (SetVars : Typ).
+Print Assumptions SetVars.t.
+End Terms_mod.