Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable from initial evars

Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot

2 files changed, 58 insertions, 0 deletions

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.