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

1 files changed, 11 insertions, 8 deletions

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;