5 files changed, 54 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7867.v b/test-suite/bugs/closed/7867.v
new file mode 100644
index 0000000000..d0c7902756
--- /dev/null
+++ b/test-suite/bugs/closed/7867.v
@@ -0,0 +1,4 @@
+(* Was a printer anomaly due to an internal lambda with no binders *)
+
+Class class := { foo : nat }.
+Fail Instance : class := { foo := 0 ; bar := 0 }.
diff --git a/test-suite/bugs/closed/8106.v b/test-suite/bugs/closed/8106.v
new file mode 100644
index 0000000000..a711c5adef
--- /dev/null
+++ b/test-suite/bugs/closed/8106.v
@@ -0,0 +1,4 @@
+(* Was raising an anomaly "already assigned a level" on the second line *)
+
+Notation "c1 ; c2" := (c1 + c2) (only printing, at level 76, right associativity, c1 at level 76, c2 at level 76).
+Notation "c1 ; c2" := (c1 + c2) (only parsing, at level 76, right associativity, c2 at level 76).
diff --git a/test-suite/bugs/closed/8121.v b/test-suite/bugs/closed/8121.v
new file mode 100644
index 0000000000..99267612ca
--- /dev/null
+++ b/test-suite/bugs/closed/8121.v
@@ -0,0 +1,46 @@
+Require Import Coq.Strings.String.
+
+Section T.
+  Eval native_compute in let x := tt in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Eval native_compute in let _ := Set in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Eval native_compute in let _ := Prop in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+End T.
+
+Section U0.
+  Let n : unit := tt.
+  Eval native_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. native_compute. Abort.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+End U0.
+
+Section S0.
+  Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "".
+  Eval native_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. native_compute. Abort.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+End S0.
+
+Class T := { }.
+Section S1.
+  Context {p : T}.
+  Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "".
+  Eval native_compute in _.
+(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. native_compute. Abort.
+(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)
+End S1.
+
+Class M := { m : Type }.
+Section S2.
+  Context {p : M}.
+  Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "".
+  Eval native_compute in _.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+  Goal exists tt : unit, tt = tt. eexists. native_compute. Abort.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+End S2.
diff --git a/test-suite/success/ssr_delayed_clear_rename.v b/test-suite/ssr/delayed_clear_rename.v
index 951e5aff79..951e5aff79 100644
--- a/test-suite/success/ssr_delayed_clear_rename.v
+++ b/test-suite/ssr/delayed_clear_rename.v
diff --git a/test-suite/ssr/ssr_rew_illtyped.v b/test-suite/ssr/rewrite_illtyped.v
index 7358068c8d..7358068c8d 100644
--- a/test-suite/ssr/ssr_rew_illtyped.v
+++ b/test-suite/ssr/rewrite_illtyped.v