5 files changed, 90 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12930.v b/test-suite/bugs/closed/bug_12930.v
new file mode 100644
index 0000000000..e2a524301a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12930.v
@@ -0,0 +1,10 @@
+Section S.
+  Variable v : Prop.
+  Variable vv : v.
+  Collection easy := Type*.
+
+  Lemma ybar : v.
+  Proof using easy.
+    exact vv.
+  Qed.
+End S.
diff --git a/test-suite/bugs/closed/bug_12944.v b/test-suite/bugs/closed/bug_12944.v
new file mode 100644
index 0000000000..d6720d9906
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12944.v
@@ -0,0 +1,12 @@
+
+Inductive vector A : nat -> Type :=
+  |nil : vector A 0
+  |cons : forall (h:A) (n:nat), vector A n -> vector A (S n).
+
+Global Set Mangle Names.
+
+Lemma vlookup_middle {A n} (v : vector A n) : True.
+Proof.
+  induction v as [|?? IHv].
+  all:exact I.
+Qed.
diff --git a/test-suite/bugs/closed/bug_4413.v b/test-suite/bugs/closed/bug_4413.v
new file mode 100644
index 0000000000..cb30aa5d1f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4413.v
@@ -0,0 +1,8 @@
+
+(* Regression wrt v8.4 related to the change of order of resolution of evar-evar unification problems. *)
+Goal exists x, x=1 -> True.
+eexists. intro H.
+pose proof (f_equal (fun k => k) H).
+Undo.
+pose (@f_equal _ _ S _ _ H).
+Abort.
diff --git a/test-suite/bugs/closed/bug_7825.v b/test-suite/bugs/closed/bug_7825.v
new file mode 100644
index 0000000000..3f8708059a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_7825.v
@@ -0,0 +1,50 @@
+Record T (x : nat) := { t : x = x }.
+
+Goal exists x, T x.
+  refine (ex_intro _ _ _).
+  Show Existentials.
+  simple refine {| t := _ |}.
+  reflexivity.
+  Unshelve. exact 0.
+Qed.
+
+(** Fine if the new evar is defined as the originally shelved evar:  we do nothing.
+  In the other direction we promote the non-shelved new goal to a shelved one:
+  shelved status has priority over goal status. *)
+
+Goal forall a : nat,  exists x, T x.
+   evar (x : nat). subst x. Show Existentials.
+   intros a. simple refine (ex_intro ?[x0] _ _). shelve. simpl.
+   (** Here ?x := ?x0 which is shelved, so ?x becomes shelved even if it would
+   not be by default (refine ?x and _ produce non-shelved evars by default)*)
+   simple refine (Build_T ?x _).
+   reflexivity.
+   Unshelve. exact 0.
+Qed.
+
+Goal { A : _ & { P : _ & @sigT A P } }.
+  epose _ as A;
+  epose _ as P;
+  exists A, P.
+  (* Regardless of which evars are in the goals vs the hypotheses,
+     [simple refine (existT _ _ _)] should leave over two goals.  This
+     should be true even when chained with epose. *)
+  assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2);
+  subst P;
+  assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2);
+  subst A;
+  assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2).
+  (* fails *)
+Abort.
+
+Goal { A : _ & { P : _ & @sigT A P } }.
+  epose _ as A;
+  epose _ as P;
+  exists A, P; (* In this example we chain everything *)
+  assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2);
+  subst P;
+  assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2);
+  subst A;
+  assert_succeeds (simple refine (existT _ _ _); let n := numgoals in guard n = 2).
+  (* fails *)
+Abort.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 73fe53c757..a39b17e1f1 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -196,3 +196,13 @@ Goal forall m n:nat, n=m.
 double induction m n.
 Abort.
 
+(* Mentioned as part of bug #12944 *)
+
+Inductive test : Set := cons : forall (IHv : nat) (v : test), test.
+
+Goal test -> test.
+induction 1 as [? IHv].
+Undo.
+destruct 1 as [? IHv].
+exact IHv. (* Check that the name is granted *)
+Qed.