diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-03 19:31:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-02 22:39:22 +0100 |
| commit | e2fa65fccb9d55ea0b6bd5873155abf436785b1f (patch) | |
| tree | 92f016008068f618703362818a4b4428729c968b | |
| parent | 6fd7634319e7a82e89667d3fc70ecbd65e7bf45c (diff) | |
When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if
possible, which is the "natural" way to orient an equation. At least
it matters for matching subterms against patterns, so that it is the
pattern variables which are substituted if ever the subterm has itself
existential variables, as in:
Goal exists x, S x = x.
eexists.
destruct (S _).
| -rw-r--r-- | pretyping/evarsolve.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3068.v | 3 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 7 |
3 files changed, 12 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index e73a5d257..328bc3bdd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1119,10 +1119,10 @@ let opp_problem = function None -> None | Some b -> Some (not b) let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env in - try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2 - with CannotProject filter1 -> try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject filter2 -> + try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2 + with CannotProject filter1 -> postpone_evar_evar f env evd pbty filter1 ev1 filter2 ev2 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v index 7cdd4ea17..03e5af61b 100644 --- a/test-suite/bugs/closed/3068.v +++ b/test-suite/bugs/closed/3068.v @@ -58,3 +58,6 @@ Section Finite_nat_set. eapply counted_list_equal_nth_char. intros i. destruct (counted_def_nth fs1 i _ ) eqn:H0. + (* This was not part of the initial bug report; this is to check that + the existential variable kept its name *) + change (true = counted_def_nth fs2 i ?def). diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 277e3ca60..d3aca59a2 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -420,4 +420,11 @@ Abort. Goal forall b:bool, b = b. intros. destruct b eqn:H. + +(* Check natural instantiation behavior when the goal has already an evar *) + +Goal exists x, S x = x. +eexists. +destruct (S _). +change (0 = ?x). Abort. |