7 files changed, 155 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5012.v b/test-suite/bugs/closed/5012.v
new file mode 100644
index 000000000..5326c0fbb
--- /dev/null
+++ b/test-suite/bugs/closed/5012.v
@@ -0,0 +1,17 @@
+Class Foo := { foo : Set }.
+
+Axiom admit : forall {T}, T.
+
+Global Instance Foo0 : Foo
+  := {| foo := admit |}.
+
+Global Instance Foo1 : Foo
+  := { foo := admit }.
+
+Existing Class Foo.
+
+Global Instance Foo2 : Foo
+  := { foo := admit }. (* Error: Unbound method name foo of class Foo. *)
+
+Set Warnings "+already-existing-class".
+Fail Existing Class Foo.
diff --git a/test-suite/bugs/closed/5696.v b/test-suite/bugs/closed/5696.v
new file mode 100644
index 000000000..a20ad1b4d
--- /dev/null
+++ b/test-suite/bugs/closed/5696.v
@@ -0,0 +1,5 @@
+(* Slightly improving interpretation of Ltac subterms in notations *)
+
+Notation "'var2' x .. y = z ; e" := (ltac:(exact z), (fun x => .. (fun y => e)
+..)) (at level 200, x binder, y binder, e at level 220).
+Check (var2 a = 1; a).
diff --git a/test-suite/bugs/closed/7695.v b/test-suite/bugs/closed/7695.v
new file mode 100644
index 000000000..42bdb076b
--- /dev/null
+++ b/test-suite/bugs/closed/7695.v
@@ -0,0 +1,20 @@
+Require Import Hurkens.
+
+Universes i j k.
+Module Type T.
+  Parameter T1 : Type@{i+1}.
+  Parameter e : Type@{j} = T1 : Type@{k}.
+End T.
+
+Module M.
+  Definition T1 := Type@{j}.
+  Definition e : Type@{j} = T1 : Type@{k} := eq_refl.
+End M.
+
+Module F (A:T).
+  Definition bad := TypeNeqSmallType.paradox _ A.e.
+End F.
+
+Set Printing Universes.
+Fail Module X := F M.
+(* Universe inconsistency. Cannot enforce j <= i because i < Coq.Logic.Hurkens.105 = j. *)
diff --git a/test-suite/bugs/closed/7712.v b/test-suite/bugs/closed/7712.v
new file mode 100644
index 000000000..a4e9697fa
--- /dev/null
+++ b/test-suite/bugs/closed/7712.v
@@ -0,0 +1,4 @@
+(* This used to raise an anomaly *)
+
+Fail Reserved Notation "'[tele_arg' x ';' .. ';' z ]"
+       (format "[tele_arg '[hv'  x .. z ']' ]").
diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v
new file mode 100644
index 000000000..216290123
--- /dev/null
+++ b/test-suite/bugs/closed/7723.v
@@ -0,0 +1,58 @@
+Set Universe Polymorphism.
+
+Module Segfault.
+
+Inductive decision_tree : Type := .
+
+Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B
+  := match ls with
+     | nil => None
+     | cons x xs
+       => match f x with
+          | Some v => Some v
+          | None => first_satisfying_helper f xs
+          end
+     end.
+
+Axiom admit : forall {T}, T.
+Definition dtree4 : option decision_tree :=
+  match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil)
+  with
+  | Some _ => admit
+  | None => admit
+  end
+.
+Definition dtree'' := Eval vm_compute in dtree4. (* segfault *)
+
+End Segfault.
+
+Module OtherExample.
+
+Definition bar@{i} := Type@{i}.
+Definition foo@{i j} (x y z : nat) :=
+  @id Type@{j} bar@{i}.
+Eval vm_compute in foo.
+
+End OtherExample.
+
+Module LocalClosure.
+
+Definition bar@{i} := Type@{i}.
+
+Definition foo@{i j} (x y z : nat) :=
+  @id (nat -> Type@{j}) (fun _ => Type@{i}).
+Eval vm_compute in foo.
+
+End LocalClosure.
+
+Require Import Hurkens.
+Polymorphic Inductive unit := tt.
+
+Polymorphic Definition foo :=
+  let x := id tt in (x, x, Type).
+
+Lemma bad : False.
+  refine (TypeNeqSmallType.paradox (snd foo) _).
+  vm_compute.
+  Fail reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/7903.v b/test-suite/bugs/closed/7903.v
new file mode 100644
index 000000000..55c7ee99a
--- /dev/null
+++ b/test-suite/bugs/closed/7903.v
@@ -0,0 +1,4 @@
+(* Slightly improving interpretation of Ltac subterms in notations *)
+
+Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)).
+Check bar x (x + x).
diff --git a/test-suite/bugs/closed/8004.v b/test-suite/bugs/closed/8004.v
new file mode 100644
index 000000000..818639997
--- /dev/null
+++ b/test-suite/bugs/closed/8004.v
@@ -0,0 +1,47 @@
+Require Export Coq.Program.Tactics Coq.Classes.SetoidTactics Coq.Classes.CMorphisms .
+
+Set Universe Polymorphism.
+
+Delimit Scope category_theory_scope with category_theory.
+Open Scope category_theory_scope.
+
+Infix "∧" := prod (at level 80, right associativity) : category_theory_scope.
+
+Class Setoid A := {
+  equiv : crelation A;
+  setoid_equiv :> Equivalence equiv
+}.
+
+Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope.
+
+Open Scope list_scope.
+
+Generalizable All Variables.
+
+Fixpoint list_equiv `{Setoid A} (xs ys : list A) : Type :=
+  match xs, ys with
+  | nil, nil => True
+  | x :: xs, y :: ys => x ≈ y ∧ list_equiv xs ys
+  | _, _ => False
+  end.
+
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+
+Program Instance list_equivalence `{Setoid A} : Equivalence list_equiv.
+Next Obligation.
+  repeat intro.
+  induction x; simpl; split; auto.
+  reflexivity.
+Qed.
+Next Obligation.
+  repeat intro.
+  generalize dependent y.
+  induction x, y; simpl; intros; auto.
+  destruct X; split.
+    now symmetry.
+  intuition.
+Qed.
+Next Obligation.
+admit.
+Defined.