From 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 5 Oct 2006 15:40:31 +0000
Subject: Correction de deux cas où les types inductifs n'étaient pas comparés
 vis à vis de l'équivalence engendrées par les modules non génératifs (cf bug
 #1242)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9215 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/closure.ml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

(limited to 'kernel/closure.ml')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6bdca4f8ff..364475019f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -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;
-- 
cgit v1.2.3