diff options
| -rw-r--r-- | pretyping/unification.ml | 8 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 17 |
2 files changed, 19 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f04a7294f1..ed01c6b7bc 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1228,12 +1228,8 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) = | e when Errors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with - | Some (evd,c1), Some (_,c2) -> - (try let evd = w_typed_unify env evd Reduction.CONV flags c1 c2 in - Some (evd, c1) - with - | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) - | e when Errors.noncritical e -> raise (NotUnifiable None)) + | Some (evd,c1) as x, Some (_,c2) -> + if is_conv env sigma c1 c2 then x else raise (NotUnifiable None) | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index fc40ea964f..4a7657e292 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -93,3 +93,20 @@ Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0. intros. destruct (g _). (* This was failing in at least r14571 *) Abort. + +(* Check that subterm selection does not solve existing evars *) + +Goal exists x, S x = S 0. +eexists. +Fail destruct (S _). (* Incompatible occurrences *) +Abort. + +Goal exists x, S 0 = S x. +eexists. +Fail destruct (S _). (* Incompatible occurrences *) +Abort. + +Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. +do 2 eexists. +Fail destruct (_, S _). (* Was succeeding at some time in trunk *) +Show Proof. |