Fixing unification of subterms identified by patterns.

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.