From be541682b63bac7ef7c67b68545c42a1cf5a53fe Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 18 Jun 2010 19:49:34 +0000
Subject: Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).

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

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 01109d8af9..690a673c6e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -239,7 +239,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       match (kind_of_term cM,kind_of_term cN) with
 	| Meta k1, Meta k2 ->
 	    let stM,stN = extract_instance_status pb in
-	    if k1 < k2
+	    if k2 < k1
 	    then sigma,(k1,cN,stN)::metasubst,evarsubst
 	    else if k1 = k2 then substn
 	    else sigma,(k2,cM,stM)::metasubst,evarsubst
-- 
cgit v1.2.3