From 41e9068a35523e66c834f3b226af2d22e97b3d2f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 12 Jun 2011 22:46:49 +0000
Subject: Oups, typo in previous commit

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

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 67990d2191..0af0aae3a7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1024,7 +1024,7 @@ let w_unify2 env flags cv_pb ty1 ty2 evd =
         secondOrderAbstraction env flags ty2 (p1,oplist1) evd
     | _, Meta p2 ->
         (* Find the predicate *)
-        secondOrderAbstraction env flags ty1 (p2, oplist2) evd in
+        secondOrderAbstraction env flags ty1 (p2, oplist2) evd
     | _ -> error "w_unify2"
 
 (* The unique unification algorithm works like this: If the pattern is
-- 
cgit v1.2.3