From 2e6c3a7b0b12cfd3b560de60f4918063f149fd01 Mon Sep 17 00:00:00 2001
From: puech
Date: Thu, 9 Oct 2008 16:05:34 +0000
Subject: * Fixed constr_cmp again to handle universes subtyping correctly *
 Fixed typo in unify_0 regarding conv_pb * First attempt to fix a problem
 related to rels in w_merge. Seems to   be unsuccessful at this point

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11443 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'pretyping/termops.ml')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d18ee4fde3..7cbde2d07b 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -946,13 +946,12 @@ let base_sort_cmp pb s0 s1 =
 
 (* eq_constr extended with universe erasure *)
 let rec constr_cmp cv_pb t1 t2 =
-  (match kind_of_term t1, kind_of_term t2 with
-       Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
-     | Prod (_,t1,c1), Prod (_,t2,c2) -> 
-	 constr_cmp Reduction.CONV t1 t2 & 
-	   constr_cmp cv_pb c1 c2
-     | _ -> false)
-  || compare_constr (constr_cmp Reduction.CONV) t1 t2
+  match kind_of_term t1, kind_of_term t2 with
+      Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
+    | Prod (_,t1,c1), Prod (_,t2,c2) -> 
+	constr_cmp Reduction.CONV t1 t2 & 
+	  constr_cmp cv_pb c1 c2
+    | _ -> compare_constr (constr_cmp Reduction.CONV) t1 t2
 
 let eq_constr = constr_cmp Reduction.CONV
 
-- 
cgit v1.2.3