6 files changed, 69 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5539.v b/test-suite/bugs/closed/5539.v
new file mode 100644
index 000000000..48e5568e9
--- /dev/null
+++ b/test-suite/bugs/closed/5539.v
@@ -0,0 +1,15 @@
+Set Universe Polymorphism.
+
+Inductive D : nat -> Type :=
+| DO : D O
+| DS n : D n -> D (S n).
+
+Fixpoint follow (n : nat) : D n -> Prop :=
+  match n with
+  | O => fun d => let 'DO := d in True
+  | S n' => fun d => (let 'DS _ d' := d in fun f => f d') (follow n')
+  end.
+
+Definition step (n : nat) (d : D n) (H : follow n d) :
+  follow (S n) (DS n d)
+  := H.
diff --git a/test-suite/bugs/closed/6770.v b/test-suite/bugs/closed/6770.v
new file mode 100644
index 000000000..9bcc74083
--- /dev/null
+++ b/test-suite/bugs/closed/6770.v
@@ -0,0 +1,7 @@
+Section visibility.
+
+  Let Fixpoint by_proof (n:nat) : True.
+  Proof. exact I. Defined.
+End visibility.
+
+Fail Check by_proof.
diff --git a/test-suite/bugs/closed/7011.v b/test-suite/bugs/closed/7011.v
new file mode 100644
index 000000000..296e4e11e
--- /dev/null
+++ b/test-suite/bugs/closed/7011.v
@@ -0,0 +1,16 @@
+(* Fix and Cofix were missing in tactic unification *)
+
+Goal exists e, (fix foo (n : nat) : nat := match n with O => e | S n' => foo n' end)
+               = (fix foo (n : nat) : nat := match n with O => O | S n' => foo n' end).
+Proof.
+  eexists.
+  reflexivity.
+Qed.
+
+CoInductive stream := cons : nat -> stream -> stream.
+
+Goal exists e, (cofix foo := cons e foo) = (cofix foo := cons 0 foo).
+Proof.
+  eexists.
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/7113.v b/test-suite/bugs/closed/7113.v
new file mode 100644
index 000000000..976e60f20
--- /dev/null
+++ b/test-suite/bugs/closed/7113.v
@@ -0,0 +1,10 @@
+Require Import Program.Tactics.
+Section visibility.
+
+  (* used to anomaly *)
+  Program Let Fixpoint ev' (n : nat) : bool := _.
+  Next Obligation. exact true. Qed.
+
+  Check ev'.
+End visibility.
+Fail Check ev'.
diff --git a/test-suite/bugs/closed/7195.v b/test-suite/bugs/closed/7195.v
new file mode 100644
index 000000000..ea97747ac
--- /dev/null
+++ b/test-suite/bugs/closed/7195.v
@@ -0,0 +1,12 @@
+(* A disjoint-names condition was missing when matching names in Ltac
+   pattern-matching *)
+
+Goal True.
+  let x := (eval cbv beta zeta in (fun P => let Q := P in fun P => P + Q)) in
+  unify x (fun a b => b + a); (* success *)
+    let x' := lazymatch x with
+              | (fun (a : ?A) (b : ?B) => ?k)
+                => constr:(fun (a : A) (b : B) => k)
+              end in
+    unify x x'.
+Abort.
diff --git a/test-suite/bugs/closed/7392.v b/test-suite/bugs/closed/7392.v
new file mode 100644
index 000000000..cf465c658
--- /dev/null
+++ b/test-suite/bugs/closed/7392.v
@@ -0,0 +1,9 @@
+Inductive R : nat -> Prop := ER : forall n, R n -> R (S n).
+
+Goal (forall (n : nat), R n -> False) -> True -> False.
+Proof.
+intros H0 H1.
+eapply H0.
+clear H1.
+apply ER.
+simpl.