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

14 files changed, 182 insertions, 139 deletions

diff --git a/.depend b/.depend
index e6539d98a..de595a4d3 100644
--- a/.depend
+++ b/.depend
@@ -925,17 +925,17 @@ parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx library/decl_kinds.cmx \
     library/libnames.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
     interp/ppextend.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \
     interp/topconstr.cmx lib/util.cmx parsing/pcoq.cmi 
-parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi parsing/coqast.cmi \
-    lib/dyn.cmi parsing/esyntax.cmi interp/genarg.cmi library/libnames.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    interp/ppextend.cmi pretyping/rawterm.cmi interp/symbols.cmi \
-    kernel/term.cmi parsing/termast.cmi interp/topconstr.cmi lib/util.cmi \
+parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi interp/constrextern.cmi \
+    parsing/coqast.cmi lib/dyn.cmi parsing/esyntax.cmi interp/genarg.cmi \
+    library/libnames.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi interp/ppextend.cmi pretyping/rawterm.cmi \
+    interp/symbols.cmi kernel/term.cmi interp/topconstr.cmi lib/util.cmi \
     parsing/ppconstr.cmi 
-parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx parsing/coqast.cmx \
-    lib/dyn.cmx parsing/esyntax.cmx interp/genarg.cmx library/libnames.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    interp/ppextend.cmx pretyping/rawterm.cmx interp/symbols.cmx \
-    kernel/term.cmx parsing/termast.cmx interp/topconstr.cmx lib/util.cmx \
+parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx interp/constrextern.cmx \
+    parsing/coqast.cmx lib/dyn.cmx parsing/esyntax.cmx interp/genarg.cmx \
+    library/libnames.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx interp/ppextend.cmx pretyping/rawterm.cmx \
+    interp/symbols.cmx kernel/term.cmx interp/topconstr.cmx lib/util.cmx \
     parsing/ppconstr.cmi 
 parsing/pptactic.cmo: kernel/closure.cmi lib/dyn.cmi parsing/egrammar.cmi \
     parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
@@ -1291,22 +1291,24 @@ proofs/evar_refiner.cmx: interp/constrintern.cmx kernel/environ.cmx \
     pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \
     proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \
     pretyping/typing.cmx lib/util.cmx proofs/evar_refiner.cmi 
-proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
-    pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \
-    kernel/inductive.cmi pretyping/inductiveops.cmi library/nameops.cmi \
-    kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
-    pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
-    pretyping/termops.cmi kernel/type_errors.cmi kernel/typeops.cmi \
-    pretyping/typing.cmi lib/util.cmi proofs/logic.cmi 
-proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
-    pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \
-    kernel/inductive.cmx pretyping/inductiveops.cmx library/nameops.cmx \
-    kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \
-    pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
-    pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \
-    pretyping/typing.cmx lib/util.cmx proofs/logic.cmi 
+proofs/logic.cmo: interp/constrextern.cmi parsing/coqast.cmi \
+    library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \
+    pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \
+    pretyping/inductiveops.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+    proofs/proof_type.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \
+    kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \
+    kernel/type_errors.cmi kernel/typeops.cmi pretyping/typing.cmi \
+    lib/util.cmi proofs/logic.cmi 
+proofs/logic.cmx: interp/constrextern.cmx parsing/coqast.cmx \
+    library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \
+    pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \
+    pretyping/inductiveops.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+    proofs/proof_type.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \
+    kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
+    kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \
+    lib/util.cmx proofs/logic.cmi 
 proofs/pfedit.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
     library/declare.cmi lib/edit.cmi kernel/entries.cmi kernel/environ.cmi \
     proofs/evar_refiner.cmi pretyping/evd.cmi library/lib.cmi \
@@ -1792,33 +1794,31 @@ toplevel/class.cmx: pretyping/classops.cmx library/decl_kinds.cmx \
 toplevel/command.cmo: toplevel/class.cmi interp/constrintern.cmi \
     library/decl_kinds.cmo kernel/declarations.cmi library/declare.cmi \
     kernel/entries.cmi kernel/environ.cmi pretyping/evarutil.cmi \
-    pretyping/evd.cmi library/global.cmi tactics/hiddentac.cmi \
-    library/impargs.cmi pretyping/indrec.cmi kernel/indtypes.cmi \
-    kernel/inductive.cmi library/lib.cmi library/libnames.cmi \
-    library/libobject.cmi library/library.cmi proofs/logic.cmi \
-    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
-    proofs/pfedit.cmi lib/pp.cmi pretyping/pretyping.cmi parsing/printer.cmi \
-    proofs/proof_type.cmi kernel/reduction.cmi proofs/refiner.cmi \
-    pretyping/retyping.cmi kernel/safe_typing.cmi library/states.cmi \
-    interp/syntax_def.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi \
-    kernel/typeops.cmi lib/util.cmi toplevel/vernacexpr.cmo \
-    toplevel/command.cmi 
+    pretyping/evd.cmi library/global.cmi library/impargs.cmi \
+    pretyping/indrec.cmi kernel/indtypes.cmi kernel/inductive.cmi \
+    library/lib.cmi library/libnames.cmi library/libobject.cmi \
+    library/library.cmi proofs/logic.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \
+    pretyping/pretyping.cmi parsing/printer.cmi proofs/proof_type.cmi \
+    kernel/reduction.cmi pretyping/retyping.cmi kernel/safe_typing.cmi \
+    library/states.cmi interp/syntax_def.cmi proofs/tacmach.cmi \
+    pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \
+    interp/topconstr.cmi kernel/typeops.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo toplevel/command.cmi 
 toplevel/command.cmx: toplevel/class.cmx interp/constrintern.cmx \
     library/decl_kinds.cmx kernel/declarations.cmx library/declare.cmx \
     kernel/entries.cmx kernel/environ.cmx pretyping/evarutil.cmx \
-    pretyping/evd.cmx library/global.cmx tactics/hiddentac.cmx \
-    library/impargs.cmx pretyping/indrec.cmx kernel/indtypes.cmx \
-    kernel/inductive.cmx library/lib.cmx library/libnames.cmx \
-    library/libobject.cmx library/library.cmx proofs/logic.cmx \
-    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
-    proofs/pfedit.cmx lib/pp.cmx pretyping/pretyping.cmx parsing/printer.cmx \
-    proofs/proof_type.cmx kernel/reduction.cmx proofs/refiner.cmx \
-    pretyping/retyping.cmx kernel/safe_typing.cmx library/states.cmx \
-    interp/syntax_def.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \
-    kernel/typeops.cmx lib/util.cmx toplevel/vernacexpr.cmx \
-    toplevel/command.cmi 
+    pretyping/evd.cmx library/global.cmx library/impargs.cmx \
+    pretyping/indrec.cmx kernel/indtypes.cmx kernel/inductive.cmx \
+    library/lib.cmx library/libnames.cmx library/libobject.cmx \
+    library/library.cmx proofs/logic.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \
+    pretyping/pretyping.cmx parsing/printer.cmx proofs/proof_type.cmx \
+    kernel/reduction.cmx pretyping/retyping.cmx kernel/safe_typing.cmx \
+    library/states.cmx interp/syntax_def.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \
+    interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx toplevel/command.cmi 
 toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \
     library/nameops.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
     lib/system.cmi toplevel/toplevel.cmi toplevel/vernac.cmi \
@@ -2578,21 +2578,21 @@ contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \
     parsing/termast.cmx lib/util.cmx toplevel/vernacexpr.cmx \
     contrib/interface/name_to_ast.cmi 
 contrib/interface/parse.cmo: contrib/interface/ascent.cmi \
-    toplevel/cerrors.cmi config/coq_config.cmi contrib/interface/ctast.cmo \
-    library/declaremods.cmi parsing/esyntax.cmi library/libnames.cmi \
-    library/libobject.cmi library/library.cmi \
-    contrib/interface/line_parser.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi lib/system.cmi \
-    lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+    toplevel/cerrors.cmi config/coq_config.cmi library/declaremods.cmi \
+    parsing/esyntax.cmi library/libnames.cmi library/libobject.cmi \
+    library/library.cmi contrib/interface/line_parser.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi \
+    lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \
+    toplevel/vernacexpr.cmo contrib/interface/vtp.cmi \
+    contrib/interface/xlate.cmi 
 contrib/interface/parse.cmx: contrib/interface/ascent.cmi \
-    toplevel/cerrors.cmx config/coq_config.cmx contrib/interface/ctast.cmx \
-    library/declaremods.cmx parsing/esyntax.cmx library/libnames.cmx \
-    library/libobject.cmx library/library.cmx \
-    contrib/interface/line_parser.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx lib/system.cmx \
-    lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
+    toplevel/cerrors.cmx config/coq_config.cmx library/declaremods.cmx \
+    parsing/esyntax.cmx library/libnames.cmx library/libobject.cmx \
+    library/library.cmx contrib/interface/line_parser.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \
+    lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \
+    toplevel/vernacexpr.cmx contrib/interface/vtp.cmx \
+    contrib/interface/xlate.cmx 
 contrib/interface/paths.cmo: contrib/interface/paths.cmi 
 contrib/interface/paths.cmx: contrib/interface/paths.cmi 
 contrib/interface/pbp.cmo: interp/coqlib.cmi contrib/interface/ctast.cmo \
@@ -2664,17 +2664,19 @@ contrib/interface/vtp.cmo: contrib/interface/ascent.cmi \
 contrib/interface/vtp.cmx: contrib/interface/ascent.cmi \
     contrib/interface/vtp.cmi 
 contrib/interface/xlate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
-    contrib/interface/ctast.cmo library/decl_kinds.cmo tactics/eauto.cmo \
-    tactics/extraargs.cmi interp/genarg.cmi library/libnames.cmi \
-    kernel/names.cmi parsing/ppconstr.cmi pretyping/rawterm.cmi \
-    proofs/tacexpr.cmo kernel/term.cmi interp/topconstr.cmi lib/util.cmi \
-    toplevel/vernacexpr.cmo contrib/interface/xlate.cmi 
+    lib/bignat.cmi contrib/interface/ctast.cmo library/decl_kinds.cmo \
+    tactics/eauto.cmo tactics/extraargs.cmi interp/genarg.cmi \
+    library/libnames.cmi kernel/names.cmi parsing/ppconstr.cmi \
+    pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \
+    interp/topconstr.cmi lib/util.cmi toplevel/vernacexpr.cmo \
+    contrib/interface/xlate.cmi 
 contrib/interface/xlate.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \
-    contrib/interface/ctast.cmx library/decl_kinds.cmx tactics/eauto.cmx \
-    tactics/extraargs.cmx interp/genarg.cmx library/libnames.cmx \
-    kernel/names.cmx parsing/ppconstr.cmx pretyping/rawterm.cmx \
-    proofs/tacexpr.cmx kernel/term.cmx interp/topconstr.cmx lib/util.cmx \
-    toplevel/vernacexpr.cmx contrib/interface/xlate.cmi 
+    lib/bignat.cmx contrib/interface/ctast.cmx library/decl_kinds.cmx \
+    tactics/eauto.cmx tactics/extraargs.cmx interp/genarg.cmx \
+    library/libnames.cmx kernel/names.cmx parsing/ppconstr.cmx \
+    pretyping/rawterm.cmx proofs/tacexpr.cmx kernel/term.cmx \
+    interp/topconstr.cmx lib/util.cmx toplevel/vernacexpr.cmx \
+    contrib/interface/xlate.cmi 
 contrib/jprover/jall.cmo: contrib/jprover/jlogic.cmi \
     contrib/jprover/jterm.cmi contrib/jprover/jtunify.cmi \
     contrib/jprover/opname.cmi contrib/jprover/jall.cmi 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ae45c932c..ee1167b8f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -168,7 +168,9 @@ and module_expr_body =
       * constraints
 
 and module_specification_body = 
-    module_type_body * module_path option * constraints
+    { msb_modtype : module_type_body;
+      msb_equiv : module_path option; 
+      msb_constraints : constraints }
 
 and structure_elem_body = 
   | SEBconst of constant_body
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e37686c40..83ea8c713 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -108,12 +108,16 @@ and module_expr_body =
   | MEBident of module_path
   | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
   | MEBstruct of mod_self_id * module_structure_body
-  | MEBapply of module_expr_body * module_expr_body
-      * constraints
+  | MEBapply of module_expr_body * module_expr_body  (* (F A) *)
+      * constraints  (* type_of(A) <: input_type_of(F) *)
 
 and module_specification_body = 
-    module_type_body * module_path option * constraints
-
+    { msb_modtype : module_type_body;
+      msb_equiv : module_path option; 
+      msb_constraints : constraints }
+    (*    type_of(equiv) <: modtype  (if given)  
+       +  substyping of past With_Module mergers *)
+    
 and structure_elem_body = 
   | SEBconst of constant_body
   | SEBmind of mutual_inductive_body
@@ -128,8 +132,8 @@ and module_body =
       mod_type : module_type_body;
       mod_equiv : module_path option;
       mod_constraints : constraints }
-
-
+    (*    type_of(mod_expr)  <: mod_user_type (if given)  *)
+    (*  if equiv given then constraints are empty *)
 
 
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index ba4dcf0b7..785e8ebdd 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -95,27 +95,34 @@ and merge_with env mtb with_decl =
 				      Some (Declarations.from_val j.uj_val);
 				    const_constraints = cst}
 		  | Some b -> 
-		      let cst1 = Reduction.conv env' c (Declarations.force b) in 
+		      let cst1 = Reduction.conv env' c (Declarations.force b) in
 		      let cst = Constraint.union cb.const_constraints cst1 in
 			SPBconst {cb with 
 				    const_body = Some (Declarations.from_val c);
 				    const_constraints = cst}
 	      end	
+(* and what about msid's ????? Don't they clash ? *)
 	| With_Module (id, mp) ->
-	    let (oldmtb,oldequiv,oldcst) = match spec with
-		SPBmodule (mtb,equiv,cst) -> (mtb,equiv,cst)
+	    let old = match spec with
+		SPBmodule msb -> msb
 	      | _ -> error_not_a_module (string_of_label l)
 	    in
 	    let mtb = type_modpath env' mp in
-	    let cst = check_subtypes env' mtb oldmtb in
+	 (* here, we should assert that there is no msid in mtb *)
+	    let cst = check_subtypes env' mtb old.msb_modtype in
 	    let equiv = 
- 	      match oldequiv with
+ 	      match old.msb_equiv with
 		| None -> Some mp
 		| Some mp' -> 
 		    check_modpath_equiv env' mp mp';
 		    Some mp
 	    in
-	      SPBmodule (mtb, equiv, Constraint.union oldcst cst)
+	    let msb =
+	      {msb_modtype = mtb; 
+	       msb_equiv = equiv; 
+	       msb_constraints = Constraint.union old.msb_constraints cst }
+	    in
+	      SPBmodule msb
       in
 	MTBsig(msid,  before@(l,new_spec)::after)
     with
@@ -135,7 +142,11 @@ and translate_entry_list env msid is_definition sig_e =
 	    add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib)
       | SPEmodule me ->
 	  let mb = translate_module env is_definition me in
-	  let mspec = mb.mod_type, mb.mod_equiv, mb.mod_constraints in
+	  let mspec = 
+	    { msb_modtype = mb.mod_type;
+	      msb_equiv = mb.mod_equiv;
+	      msb_constraints = mb.mod_constraints }
+	  in
 	  let mp' = MPdot (mp,l) in
 	    add_module mp' mb env, (l, SEBmodule mb), (l, SPBmodule mspec)
       | SPEmodtype mte ->
@@ -254,10 +265,17 @@ and add_struct_elem_constraints env = function
   | SEBmodtype mtb -> add_modtype_constraints env mtb
 
 and add_module_constraints env mb = 
+  (* if there is a body, the mb.mod_type is either inferred from the
+     body and hence uninteresting or equal to the non-empty
+     user_mod_type *)
   let env = match mb.mod_expr with
-    | None -> env
+    | None -> add_modtype_constraints env mb.mod_type
     | Some meb -> add_module_expr_constraints env meb
   in
+  let env = match mb.mod_user_type with
+    | None -> env
+    | Some mtb -> add_modtype_constraints env mtb
+  in
     Environ.add_constraints mb.mod_constraints env
 
 and add_modtype_constraints env = function
@@ -275,7 +293,7 @@ and add_modtype_constraints env = function
 and add_sig_elem_constraints env = function 
   | SPBconst cb -> Environ.add_constraints cb.const_constraints env
   | SPBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SPBmodule (mtb,_,cst) -> 
+  | SPBmodule {msb_modtype=mtb; msb_constraints=cst} -> 
       add_modtype_constraints (Environ.add_constraints cst env) mtb
   | SPBmodtype mtb -> add_modtype_constraints env mtb
 
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 ->
diff --git a/kernel/names.ml b/kernel/names.ml
index f25e6680d..7b0078392 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -246,9 +246,12 @@ module KNpred = Predicate.Make(KNord)
 module KNset = Set.Make(KNord)
 
 
-let initial_msid = (make_msid [] "TOP")
-let initial_path = MPself initial_msid
+let default_module_name = id_of_string "Top"
+
+let initial_dir = make_dirpath [default_module_name]
 
+let initial_msid = (make_msid initial_dir "Top")
+let initial_path = MPself initial_msid
 
 type variable = identifier
 type constant = kernel_name
diff --git a/kernel/names.mli b/kernel/names.mli
index 83509075e..31684371d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -125,6 +125,9 @@ val occur_mbid : mod_bound_id -> substitution -> bool
 val initial_msid : mod_self_id
 val initial_path : module_path (* [= MPself initial_msid] *)
 
+(* Initial "seed" of the unique identifier generator *)
+val initial_dir : dir_path
+
 (*s The absolute names of objects seen by kernel *)
 
 type kernel_name
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 663c6b695..f82921ba9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -36,6 +36,7 @@ type modvariant =
 type module_info = 
     { msid : mod_self_id;
       modpath : module_path;
+      seed : dir_path; (* the "seed" of unique identifier generator *)
       label : label;
       variant : modvariant}
 
@@ -72,6 +73,7 @@ let rec empty_environment =
     modinfo = {
       msid = initial_msid;
       modpath = initial_path;
+      seed = initial_dir;
       label = mk_label "_";
       variant = NONE};
     labset = Labset.empty;
@@ -220,7 +222,7 @@ let add_module l me senv =
 
 (* Interactive modules *)
 
-let start_module dir l params result senv = 
+let start_module l params result senv = 
   check_label l senv.labset; 
   let rec trans_params env = function 
     | [] -> env,[] 
@@ -240,10 +242,11 @@ let start_module dir l params result senv =
   in
   let result_body = option_app (translate_modtype env) result in
   ignore (option_app check_sig result_body);
-  let msid = make_msid dir (string_of_label l) in
+  let msid = make_msid senv.modinfo.seed (string_of_label l) in
   let mp = MPself msid in
   let modinfo = { msid = msid;
 		  modpath = mp;
+		  seed = senv.modinfo.seed;
 		  label = l;
 		  variant = STRUCT(params_body,result_body) }
   in
@@ -294,7 +297,11 @@ let end_module l senv =
       mod_equiv = None;
       mod_constraints = cst }
   in
-  let mspec = mtb, None, Constraint.empty in
+  let mspec = 
+    { msb_modtype = mtb;
+      msb_equiv = None;
+      msb_constraints = Constraint.empty } 
+  in
   let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
   let newenv = 
@@ -318,7 +325,7 @@ let end_module l senv =
 
 (* Interactive module types *)
 
-let start_modtype dir l params senv = 
+let start_modtype l params senv = 
   check_label l senv.labset; 
   let rec trans_params env = function 
     | [] -> env,[] 
@@ -331,10 +338,11 @@ let start_modtype dir l params senv =
 	env, (mbid,mtb)::transrest
   in
   let env,params_body = trans_params senv.env params in
-  let msid = make_msid dir (string_of_label l) in
+  let msid = make_msid senv.modinfo.seed (string_of_label l) in
   let mp = MPself msid in
   let modinfo = { msid = msid;
 		  modpath = mp;
+		  seed = senv.modinfo.seed;
 		  label = l;
 		  variant = SIG params_body }
   in
@@ -421,6 +429,7 @@ let start_library dir senv =
   let mp = MPself msid in
   let modinfo = { msid = msid;
 		  modpath = mp;
+		  seed = dir;
 		  label = l;
 		  variant = LIBRARY dir }
   in
@@ -456,13 +465,6 @@ let export senv dir =
     modinfo.msid, (dir,mb,senv.imports)
 
 
-let import_constraints g kn cst =
-  try
-    merge_constraints cst g
-  with UniverseInconsistency ->
-    error "import_constraints: Universe Inconsistency during import"
-
-
 let check_imports senv needed =
   let imports = senv.imports in
   let check (id,stamp) =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2d4d2403c..3efe0d16c 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -68,7 +68,7 @@ val add_constraints :
 
 (*s Interactive module functions *)
 val start_module : 
-  dir_path -> label -> (mod_bound_id * module_type_entry) list 
+  label -> (mod_bound_id * module_type_entry) list 
     -> module_type_entry option 
       -> safe_environment -> module_path * safe_environment
 
@@ -77,7 +77,7 @@ val end_module :
 
 
 val start_modtype :
-  dir_path -> label -> (mod_bound_id * module_type_entry) list
+  label -> (mod_bound_id * module_type_entry) list
     -> safe_environment -> module_path * safe_environment
 
 val end_modtype :
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bf53c6965..6b0931a9e 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -163,13 +163,12 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
 	  in
 	    check_conv cst conv env c1 c2
 	      
-let rec check_modules cst env msid1 l 
-  (mtb1,mpo1,cst1 as msb1) (mtb2,mpo2,cst2 as msb2) =
+let rec check_modules cst env msid1 l msb1 msb2 =
   let mp = (MPdot(MPself msid1,l)) in
-  let mty1 = strengthen env mtb1 mp in
-  let cst = check_modtypes cst env mty1 mtb2 false in
+  let mty1 = strengthen env msb1.msb_modtype mp in
+  let cst = check_modtypes cst env mty1 msb2.msb_modtype false in
   begin
-    match mpo1, mpo2 with
+    match msb1.msb_equiv, msb2.msb_equiv with
       | _, None -> ()
       | None, Some mp2 -> 
 	  check_modpath_equiv env mp mp2
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 7b6c7ec1b..7321801d2 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -438,7 +438,7 @@ let start_module interp_modtype id args res_o =
   let arg_entries = List.concat (List.rev arg_entries_revlist) in
   let res_entry_o = option_app (interp_modtype env) res_o in
 
-  let mp = Global.start_module (Lib.module_dp()) id arg_entries res_entry_o in
+  let mp = Global.start_module id arg_entries res_entry_o in
 
   let mbids = List.map fst arg_entries in
   openmod_info:=(mbids,res_entry_o);
@@ -560,7 +560,7 @@ let start_modtype interp_modtype id args =
   in
   let arg_entries = List.concat (List.rev arg_entries_revlist) in
 
-  let mp = Global.start_modtype (Lib.module_dp()) id arg_entries in
+  let mp = Global.start_modtype id arg_entries in
 
   let mbids = List.map fst arg_entries in
   openmodtype_info := mbids;
diff --git a/library/global.ml b/library/global.ml
index cdebc52f5..4824f0b2f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -69,9 +69,9 @@ let add_constraints c = global_env := add_constraints c !global_env
 
 
 
-let start_module dir id params mtyo =
+let start_module id params mtyo =
   let l = label_of_id id in
-  let mp,newenv = start_module dir l params mtyo !global_env in
+  let mp,newenv = start_module l params mtyo !global_env in
     global_env := newenv;
     mp
   
@@ -82,9 +82,9 @@ let end_module id =
     mp
 
 
-let start_modtype dir id params = 
+let start_modtype id params = 
   let l = label_of_id id in
-  let mp,newenv = start_modtype dir l params !global_env in
+  let mp,newenv = start_modtype l params !global_env in
     global_env := newenv;
     mp
 
diff --git a/library/global.mli b/library/global.mli
index 4a215167a..72d3731df 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -57,7 +57,7 @@ val add_constraints : constraints -> unit
    of the started module / module type *)
 
 val start_module : 
-  dir_path -> identifier -> (mod_bound_id * module_type_entry) list 
+  identifier -> (mod_bound_id * module_type_entry) list 
     -> module_type_entry option 
       -> module_path
 
@@ -65,7 +65,7 @@ val end_module :
   identifier -> module_path
 
 val start_modtype :
-  dir_path -> identifier -> (mod_bound_id * module_type_entry) list
+  identifier -> (mod_bound_id * module_type_entry) list
     -> module_path
 
 val end_modtype :
diff --git a/library/nameops.ml b/library/nameops.ml
index a61ba754b..7a4b67b84 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -147,8 +147,7 @@ let next_name_away name l =
 
 let pr_lab l = str (string_of_label l)
 
-let default_module_name = id_of_string "Top"
-let default_module = make_dirpath [default_module_name]
+let default_module = Names.initial_dir (* = ["Top"] *)
 
 (*s Roots of the space of absolute names *)
 let coq_root = id_of_string "Coq"