Corrections de gestion des univers et modules + meilleure gestions des noms uniques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 29 insertions, 18 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index a75f2d483..cd8cbe1ee 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -70,13 +70,13 @@ let rec scrape_modtype env = function
   | MTBident kn -> scrape_modtype env (lookup_modtype kn env)
   | mtb -> mtb
 
-
-let module_body_of_spec (mty,mpo,cst) = 
-    { mod_type = mty;
-      mod_equiv = mpo;
+(* the constraints are not important here *)
+let module_body_of_spec msb = 
+    { mod_type = msb.msb_modtype;
+      mod_equiv = msb.msb_equiv;
       mod_expr = None;
       mod_user_type = None;
-      mod_constraints = cst}
+      mod_constraints = Constraint.empty}
 
 let module_body_of_type mtb = 
   { mod_type = mtb;
@@ -86,7 +86,13 @@ let module_body_of_type mtb =
     mod_constraints = Constraint.empty}
 
 
-let module_spec_of_body mb = mb.mod_type, mb.mod_equiv, mb.mod_constraints
+(* the constraints are not important here *)
+let module_spec_of_body mb = 
+  { msb_modtype = mb.mod_type; 
+    msb_equiv = mb.mod_equiv; 
+    msb_constraints = Constraint.empty}
+
+
 
 let destr_functor = function
   | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
@@ -129,11 +135,14 @@ and subst_signature sub sign =
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
 
-and subst_module sub (mtb,mpo,cst as mb) =
-  let mtb' = subst_modtype sub mtb in
-  let mpo' = option_smartmap (subst_mp sub) mpo in
-    if mtb'==mtb && mpo'==mpo then mb else
-      (mtb',mpo',cst)
+and subst_module sub mb =
+  let mtb' = subst_modtype sub mb.msb_modtype in
+  let mpo' = option_smartmap (subst_mp sub) mb.msb_equiv in
+    if mtb'==mb.msb_modtype && mpo'==mb.msb_equiv then mb else
+      { msb_modtype=mtb'; 
+	msb_equiv=mpo'; 
+	msb_constraints=mb.msb_constraints}
+
 
 let subst_signature_msid msid mp = 
   subst_signature (map_msid msid mp)
@@ -179,13 +188,15 @@ let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with
   | MTBident _ -> anomaly "scrape_modtype does not work!"
   | MTBfunsig _ -> mtb
   | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp)
-and strengthen_mod env mp (mtb,mpo,cst) = 
-  let mtb' = strengthen_mtb env mp mtb in
-  let mpo' = match mpo with
-    | Some _ -> mpo
-    | None -> Some mp
-  in
-    (mtb',mpo',cst)
+
+and strengthen_mod env mp msb = 
+  { msb_modtype = strengthen_mtb env mp msb.msb_modtype;
+    msb_equiv = begin match msb.msb_equiv with
+      | Some _ -> msb.msb_equiv
+      | None -> Some mp 
+    end ;
+    msb_constraints = msb.msb_constraints; }
+
 and strengthen_sig env msid sign mp = match sign with
   | [] -> []
   | (l,SPBconst cb) :: rest ->