Refine test for unresolved evars: not reachable from initial evars

The test is refined to handle aliases: i.e. undefined evars coming from
restrictions and evar-evar unifications with an initial evar are not
considered fresh unresolved evars. To check this, we generalize the
restricted_evars set to an aliased_evars set in the evar map,
registering evars being solved by another evar due to restriction
or evar-evar unifications. This implements the proposal of PR #370
for testing the resolution status of evars independently of the evar-evar
orientation order.

This allows [apply] to refine an evar with a new one if it results from a
[clear] request or an evar-evar solution only, otherwise the new evar is
considered fresh and an error is raised.

Also fixes bugs #4095 and #4413.

Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>

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.