5 files changed, 44 insertions, 50 deletions
diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v
deleted file mode 100644
index 8c26af708b..0000000000
--- a/test-suite/bugs/closed/4882.v
+++ /dev/null
@@ -1,50 +0,0 @@
-
-Definition Foo {T}{a : T} : T := a.
-
-Module A.
-
-  Declare Implicit Tactic eauto.
-
-  Goal forall A (x : A), A.
-  intros.
-  apply Foo. (* Check defined evars are normalized *)
-  (*  Qed. *)
-  Abort.
-
-End A.
-
-Module B.
-
-  Definition Foo {T}{a : T} : T := a.
-
-  Declare Implicit Tactic eassumption.
-
-  Goal forall A (x : A), A.
-  intros.
-  apply Foo.
-  (*  Qed. *)
-  Abort.
-
-End B.
-
-Module C.
-
-  Declare Implicit Tactic first [exact True|assumption].
-
-  Goal forall (x : True), True.
-  intros.
-  apply (@Foo _ _).
-  Qed.
-
-End C.
-
-Module D.
-
-  Declare Implicit Tactic assumption.
-
-  Goal forall A (x : A), A.
-  intros.
-  exact _.
-  Qed.
-
-End D.
diff --git a/test-suite/bugs/closed/5539.v b/test-suite/bugs/closed/5539.v
new file mode 100644
index 0000000000..48e5568e9b
--- /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 0000000000..9bcc740830
--- /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/7113.v b/test-suite/bugs/closed/7113.v
new file mode 100644
index 0000000000..976e60f20c
--- /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 0000000000..ea97747ac9
--- /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.