diff options
| -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. |