5 files changed, 88 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2733.v b/test-suite/bugs/closed/2733.v
index 832de4f913..24dd30b32e 100644
--- a/test-suite/bugs/closed/2733.v
+++ b/test-suite/bugs/closed/2733.v
@@ -16,6 +16,21 @@ match k,l with
  |B,l' => Bcons true (Ncons 0 l')
 end.
 
+(* At some time, the success of trullynul was dependent on the name of
+   the variables! *)
+
+Definition trullynul2 k {a} (l : alt_list k a) :=
+match k,l with
+ |N,l' => Ncons 0 (Bcons true l')
+ |B,l' => Bcons true (Ncons 0 l')
+end.
+
+Definition trullynul3 k {z} (l : alt_list k z) :=
+match k,l with
+ |N,l' => Ncons 0 (Bcons true l')
+ |B,l' => Bcons true (Ncons 0 l')
+end.
+
 Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 ->
 alt_list t1 t3 :=
   match l with
diff --git a/test-suite/bugs/closed/7854.v b/test-suite/bugs/closed/7854.v
new file mode 100644
index 0000000000..ab1a29b632
--- /dev/null
+++ b/test-suite/bugs/closed/7854.v
@@ -0,0 +1,10 @@
+Set Primitive Projections.
+
+CoInductive stream (A : Type) := cons {
+  hd : A;
+  tl : stream A;
+}.
+
+CoFixpoint const {A} (x : A) := cons A x (const x).
+
+Check (@eq_refl _ (const tt) <<: tl unit (const tt) = const tt).
diff --git a/test-suite/bugs/closed/8081.v b/test-suite/bugs/closed/8081.v
new file mode 100644
index 0000000000..0f2501aaa8
--- /dev/null
+++ b/test-suite/bugs/closed/8081.v
@@ -0,0 +1,4 @@
+Section foo.
+End foo.
+Section foo.
+End foo.
diff --git a/test-suite/bugs/closed/8119.v b/test-suite/bugs/closed/8119.v
new file mode 100644
index 0000000000..c6329a7328
--- /dev/null
+++ b/test-suite/bugs/closed/8119.v
@@ -0,0 +1,46 @@
+Require Import Coq.Strings.String.
+
+Section T.
+  Eval vm_compute in let x := tt in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Eval vm_compute in let _ := Set in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Eval vm_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 vm_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. vm_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 vm_compute in _.
+(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. vm_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 vm_compute in _.
+(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)
+  Goal exists tt : unit, tt = tt. eexists. vm_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 vm_compute in _.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+  Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort.
+(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *)
+End S2.
diff --git a/test-suite/bugs/closed/8126.v b/test-suite/bugs/closed/8126.v
new file mode 100644
index 0000000000..f52dfc6b47
--- /dev/null
+++ b/test-suite/bugs/closed/8126.v
@@ -0,0 +1,13 @@
+(* See also output test Notations4.v *)
+
+Inductive foo := tt.
+Bind Scope foo_scope with foo.
+Delimit Scope foo_scope with foo.
+Notation "'HI'" := tt : foo_scope.
+Definition myfoo (x : nat) (y : nat) (z : foo) := y.
+Notation myfoo0 := (@myfoo 0).
+Notation myfoo01 := (@myfoo0 1).
+Check myfoo 0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI]  *)
+Check myfoo0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI]  *)
+Check myfoo01 tt. (* prints [myfoo0 1 HI], but should print [myfoo01 HI]  *)
+Check myfoo01 HI. (* was failing *)