From efa1c32a4d17870794dbc6f0301c3c0d46637a55 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 9 Aug 2014 18:53:21 +0200
Subject: Fixing unification of subterms identified by patterns.

---
 pretyping/unification.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3