From b6dabf6aa5b96cfa3c11038316399f0797d734ac Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 25 Apr 2017 21:54:31 +0200 Subject: 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 --- test-suite/bugs/closed/bug_4413.v | 8 +++++++ test-suite/bugs/closed/bug_7825.v | 50 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+) create mode 100644 test-suite/bugs/closed/bug_4413.v create mode 100644 test-suite/bugs/closed/bug_7825.v (limited to 'test-suite') 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. -- cgit v1.2.3