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

5 files changed, 22 insertions, 17 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6bdca4f8f..364475019 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;
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 88f9139e6..2a0c1f89e 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -179,8 +179,9 @@ val whd_stack :
 (* [unfold_reference] unfolds references in a [fconstr] *)
 val unfold_reference : clos_infos -> table_key -> fconstr option
 
-(* [mind_equiv] checks whether two mutual inductives are intentionally equal *)
-val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool
+(* [mind_equiv] checks whether two inductive types are intentionally equal *)
+val mind_equiv : env -> inductive -> inductive -> bool
+val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
 
 (************************************************************************)
 (*i This is for lazy debug *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2e2bcafce..d62af2e5e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -364,7 +364,7 @@ let inductive_equiv env (kn1,i1) (kn2,i2) =
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    (indsp <> ci.ci_ind) or
+    not (Closure.mind_equiv env indsp ci.ci_ind) or
     (mib.mind_nparams <> ci.ci_npar) or
     (mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5b69ac7b6..28176ecc5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -257,14 +257,14 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
 
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
-     | (FInd (kn1,i1), FInd (kn2,i2)) ->
-         if i1 = i2 && mind_equiv infos kn1 kn2
+     | (FInd ind1, FInd ind2) ->
+         if mind_equiv_infos infos ind1 ind2
 	 then
            convert_stacks infos lft1 lft2 v1 v2 cuniv
          else raise NotConvertible
 
-     | (FConstruct ((kn1,i1),j1), FConstruct ((kn2,i2),j2)) ->
-	 if i1 = i2 && j1 = j2 && mind_equiv infos kn1 kn2
+     | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
+	 if j1 = j2 && mind_equiv_infos infos ind1 ind2
 	 then
            convert_stacks infos lft1 lft2 v1 v2 cuniv
          else raise NotConvertible
@@ -317,7 +317,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
 and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks
     (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c)
-    (fun (mind1,i1) (mind2,i2) -> i1=i2 && mind_equiv infos mind1 mind2)
+    (mind_equiv_infos infos)
     lft1 stk1 lft2 stk2 cuniv
 
 and convert_vect infos lft1 lft2 v1 v2 cuniv =
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 7115097e4..7c515735d 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -83,7 +83,8 @@ and conv_whd pb k whd1 whd2 cu =
 and conv_atom pb k a1 stk1 a2 stk2 cu =
   match a1, a2 with
   | Aind (kn1,i1), Aind(kn2,i2) ->
-      if i1 = i2 && mind_equiv !infos kn1 kn2 && compare_stack stk1 stk2 then
+      if mind_equiv_infos !infos (kn1,i1) (kn2,i2) && compare_stack stk1 stk2
+      then
 	conv_stack k stk1 stk2 cu
       else raise NotConvertible
   | Aid ik1, Aid ik2 ->