Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 22 insertions, 13 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bbc89e39..9a8de5a9 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml 8845 2006-05-23 07:41:58Z herbelin $ i*)
+(*i $Id: subtyping.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -94,9 +94,9 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       (* listrec ignored *)
       (* finite done *)
       (* nparams done *)
-      (* params_ctxt done *)
+      (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let cst = check_conv cst conv env (type_of_inductive (mib1,p1)) (type_of_inductive (mib2,p2))
+      let cst = check_conv cst conv env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
       in
 	cst
   in
@@ -114,9 +114,12 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
   assert (Array.length mib1.mind_packets >= 1 
 	    && Array.length mib2.mind_packets >= 1);
 
-       (* TODO: we should allow renaming of parameters at least ! *)
+  (* Check that the expected numbers of uniform parameters are the same *)
+  (* No need to check the contexts of parameters: it is checked *)
+  (* at the time of checking the inductive arities in check_packet. *)
+  (* Notice that we don't expect the local definitions to match: only *)
+  (* the inductive types and constructors types have to be convertible *)
   check (fun mib -> mib.mind_nparams);
-  check (fun mib -> mib.mind_params_ctxt); 
 
   begin 
     match mib2.mind_equiv with
@@ -161,7 +164,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
    | Constant cb1 ->
       assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
       (*Start by checking types*)
-      let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in
+      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+      let cst = check_conv cst conv_leq env typ1 typ2 in
       let con = make_con (MPself msid1) empty_dirpath l in
       let cst =
        match cb2.const_body with
@@ -176,23 +181,27 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
       in
        cst
    | IndType ((kn,i),mind1) ->
-      Util.error ("The kernel does not recognize yet that a parameter can be " ^
+      ignore (Util.error (
+       "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by an inductive type. Hint: you can rename the " ^
        "inductive type and give a definition to map the old name to the new " ^
-       "name.") ;
+       "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if cb2.const_body <> None then error () ;
-      let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in
-       check_conv cst conv_leq env arity1 cb2.const_type
+      let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+       check_conv cst conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
-      Util.error ("The kernel does not recognize yet that a parameter can be " ^
+      ignore (Util.error (
+       "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
-       "name.") ;
+       "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if cb2.const_body <> None then error () ;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
-       check_conv cst conv env ty1 cb2.const_type
+      let ty2 = Typeops.type_of_constant_type env cb2.const_type in
+       check_conv cst conv env ty1 ty2
    | _ -> error ()
 	      
 let rec check_modules cst env msid1 l msb1 msb2 =