Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 12 insertions, 9 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 617611bf..41fe8750 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: closure.ml 8802 2006-05-10 20:47:28Z barras $ *)
+(* $Id: closure.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
 
 open Util
 open Pp
@@ -375,14 +375,17 @@ let defined_rels flags env =
       (rel_context env) ~init:(0,[])
 (*  else (0,[])*)
 
-
-let rec mind_equiv info kn1 kn2 = 
-  kn1 = kn2 ||
-	match (lookup_mind kn1 info.i_env).mind_equiv with
-	    Some kn1' -> mind_equiv info kn2 kn1'
-	  | None -> match (lookup_mind kn2 info.i_env).mind_equiv with
-		Some kn2' -> mind_equiv info kn2' kn1
-	      | None -> false
+let rec mind_equiv env (kn1,i1) (kn2,i2) =
+  let rec equiv kn1 kn2 =
+    kn1 = kn2 ||
+      match (lookup_mind kn1 env).mind_equiv with
+	  Some kn1' -> equiv kn2 kn1'
+	| None -> match (lookup_mind kn2 env).mind_equiv with
+	      Some kn2' -> equiv kn2' kn1
+	    | None -> false in
+  i1 = i2 && equiv kn1 kn2
+
+let mind_equiv_infos info = mind_equiv info.i_env
 
 let create mk_cl flgs env =
   { i_flags = flgs;