From bef7efb2c9c398e7f9fd7e38ece6f5a3c99461f3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 12 Jun 2011 22:27:49 +0000
Subject: Removed what looks like a (very old) useless f.o. unification pass
 made after s.o. unification succeeds.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14191 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/unification.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d09e5f2451..67990d2191 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1021,16 +1021,10 @@ let w_unify2 env flags cv_pb ty1 ty2 evd =
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
-	let evd' =
-          secondOrderAbstraction env flags ty2 (p1,oplist1) evd in
-        (* Resume first order unification *)
-	w_unify_0 env cv_pb flags (nf_meta evd' ty1) ty2 evd'
+        secondOrderAbstraction env flags ty2 (p1,oplist1) evd
     | _, Meta p2 ->
         (* Find the predicate *)
-	let evd' =
-          secondOrderAbstraction env flags ty1 (p2, oplist2) evd in
-        (* Resume first order unification *)
-	w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd'
+        secondOrderAbstraction env flags ty1 (p2, oplist2) evd in
     | _ -> error "w_unify2"
 
 (* The unique unification algorithm works like this: If the pattern is
-- 
cgit v1.2.3