La notation with dependante + affichage dependante de moduels corrige

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

9 files changed, 303 insertions, 263 deletions

diff --git a/.depend b/.depend
index 7a1679545..59bd9eab8 100644
--- a/.depend
+++ b/.depend
@@ -42,9 +42,9 @@ library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
     library/nametab.cmi kernel/safe_typing.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/univ.cmi 
-library/declaremods.cmi: kernel/entries.cmi library/lib.cmi \
-    library/libnames.cmi library/libobject.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/safe_typing.cmi 
+library/declaremods.cmi: kernel/entries.cmi kernel/environ.cmi \
+    library/lib.cmi library/libnames.cmi library/libobject.cmi \
+    kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi 
 library/global.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/indtypes.cmi library/libnames.cmi \
     kernel/names.cmi kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \
@@ -387,6 +387,7 @@ contrib/jprover/jlogic.cmi: contrib/jprover/jterm.cmi
 contrib/jprover/jterm.cmi: contrib/jprover/opname.cmi 
 contrib/xml/xmlcommand.cmi: library/libnames.cmi kernel/names.cmi \
     lib/util.cmi 
+tmp/Discharge/libnames.cmi: kernel/names.cmi lib/pp.cmi lib/predicate.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi 
@@ -576,15 +577,15 @@ library/declare.cmx: kernel/declarations.cmx kernel/entries.cmx \
     library/summary.cmx kernel/term.cmx kernel/type_errors.cmx \
     kernel/typeops.cmx kernel/univ.cmx lib/util.cmx library/declare.cmi 
 library/declaremods.cmo: kernel/declarations.cmi kernel/entries.cmi \
-    library/global.cmi library/lib.cmi library/libnames.cmi \
-    library/libobject.cmi kernel/modops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/pp.cmi library/summary.cmi lib/util.cmi \
-    library/declaremods.cmi 
+    kernel/environ.cmi library/global.cmi library/lib.cmi \
+    library/libnames.cmi library/libobject.cmi kernel/modops.cmi \
+    kernel/names.cmi library/nametab.cmi lib/pp.cmi library/summary.cmi \
+    lib/util.cmi library/declaremods.cmi 
 library/declaremods.cmx: kernel/declarations.cmx kernel/entries.cmx \
-    library/global.cmx library/lib.cmx library/libnames.cmx \
-    library/libobject.cmx kernel/modops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/pp.cmx library/summary.cmx lib/util.cmx \
-    library/declaremods.cmi 
+    kernel/environ.cmx library/global.cmx library/lib.cmx \
+    library/libnames.cmx library/libobject.cmx kernel/modops.cmx \
+    kernel/names.cmx library/nametab.cmx lib/pp.cmx library/summary.cmx \
+    lib/util.cmx library/declaremods.cmi 
 library/global.cmo: kernel/environ.cmi kernel/inductive.cmi \
     library/libnames.cmi kernel/names.cmi kernel/safe_typing.cmi \
     kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
@@ -674,13 +675,11 @@ parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx parsing/genarg.cmx \
     library/libnames.cmx kernel/names.cmx lib/pp.cmx proofs/tacexpr.cmx \
     lib/util.cmx parsing/ast.cmi 
 parsing/astmod.cmo: parsing/astterm.cmi parsing/coqast.cmi kernel/entries.cmi \
-    pretyping/evd.cmi library/global.cmi library/lib.cmi library/libnames.cmi \
-    kernel/modops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    lib/util.cmi parsing/astmod.cmi 
+    pretyping/evd.cmi library/libnames.cmi kernel/modops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi lib/util.cmi parsing/astmod.cmi 
 parsing/astmod.cmx: parsing/astterm.cmx parsing/coqast.cmx kernel/entries.cmx \
-    pretyping/evd.cmx library/global.cmx library/lib.cmx library/libnames.cmx \
-    kernel/modops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    lib/util.cmx parsing/astmod.cmi 
+    pretyping/evd.cmx library/libnames.cmx kernel/modops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx lib/util.cmx parsing/astmod.cmi 
 parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     lib/dyn.cmi kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
     library/global.cmi library/impargs.cmi library/libnames.cmi \
@@ -867,14 +866,12 @@ parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \
     parsing/ppconstr.cmx kernel/sign.cmx kernel/term.cmx parsing/termast.cmx \
     pretyping/termops.cmx lib/util.cmx parsing/printer.cmi 
-parsing/printmod.cmo: kernel/declarations.cmi kernel/environ.cmi \
-    library/global.cmi library/libnames.cmi library/nameops.cmi \
-    kernel/names.cmi library/nametab.cmi lib/pp.cmi lib/util.cmi \
-    parsing/printmod.cmi 
-parsing/printmod.cmx: kernel/declarations.cmx kernel/environ.cmx \
-    library/global.cmx library/libnames.cmx library/nameops.cmx \
-    kernel/names.cmx library/nametab.cmx lib/pp.cmx lib/util.cmx \
-    parsing/printmod.cmi 
+parsing/printmod.cmo: kernel/declarations.cmi library/global.cmi \
+    library/libnames.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi lib/pp.cmi lib/util.cmi parsing/printmod.cmi 
+parsing/printmod.cmx: kernel/declarations.cmx library/global.cmx \
+    library/libnames.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx lib/pp.cmx lib/util.cmx parsing/printmod.cmi 
 parsing/q_coqast.cmo: parsing/coqast.cmi parsing/genarg.cmi \
     library/libnames.cmi kernel/names.cmi parsing/pcoq.cmi parsing/q_util.cmi \
     pretyping/rawterm.cmi proofs/tacexpr.cmo 
@@ -1657,6 +1654,14 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
     kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
     lib/util.cmx tactics/wcclausenv.cmi 
+tmp/probj.cmo: library/declaremods.cmi library/libobject.cmi 
+tmp/probj.cmx: library/declaremods.cmx library/libobject.cmx 
+tmp/vernacentries.cmo: parsing/ast.cmi toplevel/class.cmi \
+    toplevel/command.cmi library/declare.cmi library/libnames.cmi \
+    tactics/tactics.cmi 
+tmp/vernacentries.cmx: parsing/ast.cmx toplevel/class.cmx \
+    toplevel/command.cmx library/declare.cmx library/libnames.cmx \
+    tactics/tactics.cmx 
 tools/coqdep_lexer.cmo: config/coq_config.cmi 
 tools/coqdep_lexer.cmx: config/coq_config.cmx 
 tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
@@ -2707,6 +2712,26 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx 
 contrib/xml/xml.cmo: contrib/xml/xml.cmi 
 contrib/xml/xml.cmx: contrib/xml/xml.cmi 
+tmp/Discharge/declare.cmo: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi library/global.cmi library/impargs.cmi \
+    kernel/indtypes.cmi kernel/inductive.cmi library/lib.cmi \
+    library/libnames.cmi library/libobject.cmi library/library.cmi \
+    library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    kernel/reduction.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+    library/summary.cmi kernel/term.cmi kernel/type_errors.cmi \
+    kernel/typeops.cmi kernel/univ.cmi lib/util.cmi 
+tmp/Discharge/declare.cmx: kernel/declarations.cmx kernel/entries.cmx \
+    kernel/environ.cmx library/global.cmx library/impargs.cmx \
+    kernel/indtypes.cmx kernel/inductive.cmx library/lib.cmx \
+    library/libnames.cmx library/libobject.cmx library/library.cmx \
+    library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+    kernel/reduction.cmx kernel/safe_typing.cmx kernel/sign.cmx \
+    library/summary.cmx kernel/term.cmx kernel/type_errors.cmx \
+    kernel/typeops.cmx kernel/univ.cmx lib/util.cmx 
+tmp/Discharge/libnames.cmo: kernel/names.cmi lib/pp.cmi lib/predicate.cmi \
+    lib/util.cmi tmp/Discharge/libnames.cmi 
+tmp/Discharge/libnames.cmx: kernel/names.cmx lib/pp.cmx lib/predicate.cmx \
+    lib/util.cmx tmp/Discharge/libnames.cmi 
 tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 tactics/tauto.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 tactics/eqdecide.cmo: parsing/grammar.cma
diff --git a/dev/Makefile.devel b/dev/Makefile.devel
index 78318d59b..729e6147e 100644
--- a/dev/Makefile.devel
+++ b/dev/Makefile.devel
@@ -43,4 +43,4 @@ total:
 
 #runs coqtop storing using the history file
 run:	$(TOPDIR)/coqtop
-	ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop
+	ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 2c00fe52e..0fb79376a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -162,7 +162,9 @@ and translate_module env is_definition me =
     | Some mexpr, _ -> 
 	let meq_o = (* do we have a transparent module ? *)
 	  try       (* TODO: transparent field in module_entry *)
-	    Some (path_of_mexpr mexpr)
+	    match me.mod_entry_type with
+	      | None -> Some (path_of_mexpr mexpr)
+	      | Some _ -> None
 	  with 
 	    | Not_path -> None
 	in
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 28817ebe4..4169fa56f 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -155,7 +155,8 @@ let do_module exists what iter_objects i dir mp substobjs objects =
       | None ->  ()
 
     
-let conv_names_do_module exists what iter_objects i (sp,kn) substobjs substituted =
+let conv_names_do_module exists what iter_objects i 
+      (sp,kn) substobjs substituted =
   let dir,mp = dir_of_sp sp, mp_of_kn kn in
   do_module exists what iter_objects i dir mp substobjs substituted
 
@@ -389,42 +390,60 @@ let process_module_bindings argids args =
     let mp = MPbound mbid in
     let substobjs = get_modtype_substobjs mty in
     let substituted = subst_substobjs dir mp substobjs in
-      do_module false "begin" load_objects 1 dir mp substobjs substituted
+      do_module false "start" load_objects 1 dir mp substobjs substituted
   in
     List.iter2 process_arg argids args
 
-(*
-(* this function removes keep objects from submodules *) 
-let rec kill_keep objs =
-  let kill = function
-    | (oname,Leaf obj) as node ->
-	if object_tag obj = "MODULE" then
-	  let (entry,substobjs,substitute) = out_module obj in
-	    match substitute,keep with
-	      | [],[] -> node
-	      | _ -> oname, Leaf (in_module (entry,(substobjs,[],[])))
-	else
-	  node
-    | _ -> anomaly "kill_keep expects Leafs only!"
-  in
-    match objs with
-      | [] -> objs
-      | h::tl -> let h'=kill h and tl'=kill_keep tl in
-	  if h==h' && tl==tl' then
-	    objs
-	  else
-	    h'::tl'
-*)
 
-let start_module id argids args res_o =
-  let mp = Global.start_module (Lib.module_dp()) id args res_o in
-  let mbids = List.map fst args in
+let replace_module mtb id mb = todo "replace module after with"; mtb 
+
+let rec get_some_body mty env = match mty with
+    MTEident kn -> Environ.lookup_modtype kn env 
+  | MTEfunsig _ 
+  | MTEsig _ -> anomaly "anonymous module types not supported"
+  | MTEwith (mty,With_Definition _) -> get_some_body mty env 
+  | MTEwith (mty,With_Module (id,mp)) -> 
+      replace_module (get_some_body mty env) id (Environ.lookup_module mp env)
+
+
+let intern_args interp_modtype (env,oldargs) (idl,arg) = 
+  let lib_dir = Lib.module_dp() in
+  let mbids = List.map (fun id -> make_mbid lib_dir (string_of_id id)) idl in
+  let mty = interp_modtype env arg in
+  let dirs = List.map (fun id -> make_dirpath [id]) idl in
+  let mps = List.map (fun mbid -> MPbound mbid) mbids in
+  let substobjs = get_modtype_substobjs mty in
+  let substituted's = 
+    List.map2 
+      (fun dir mp -> dir, mp, subst_substobjs dir mp substobjs) 
+      dirs mps  
+  in
+    List.iter 
+      (fun (dir, mp, substituted) -> 
+	 do_module false "interp" load_objects 1 dir mp substobjs substituted)
+      substituted's;
+    let body = Modops.module_body_of_type (get_some_body mty env) in
+    let env = 
+      List.fold_left (fun env mp -> Modops.add_module mp body env) env mps
+    in
+    env, List.map (fun mbid -> mbid,mty) mbids :: oldargs
+      
+let start_module interp_modtype id args res_o =
   let fs = Summary.freeze_summaries () in
-    process_module_bindings argids args;
-    openmod_info:=(mbids,res_o);
-    let prefix = Lib.start_module id mp fs in
-    Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
-    Lib.add_frozen_state ()
+  let env = Global.env () in
+  let env,arg_entries_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  in
+  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 mbids = List.map fst arg_entries in
+  openmod_info:=(mbids,res_entry_o);
+  let prefix = Lib.start_module id mp fs in
+  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
+  Lib.add_frozen_state ()
 
 
 let end_module id =
@@ -478,7 +497,7 @@ let module_objects mp =
 
 type library_name = dir_path
 
-(* The first two will form a substitutive_objects, the last one is keep *)
+(* The first two will form substitutive_objects, the last one is keep *)
 type library_objects = 
     mod_self_id * lib_objects * lib_objects
 
@@ -532,14 +551,21 @@ let import_module mp =
     open_objects 1 prefix objects
 
 
-let start_modtype id argids args =
-  let mp = Global.start_modtype (Lib.module_dp()) id args in
-  let fs= Summary.freeze_summaries () in
-    process_module_bindings argids args;
-    openmodtype_info := (List.map fst args);
-    let prefix = Lib.start_modtype id mp fs in
-    Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
-    Lib.add_frozen_state ()
+let start_modtype interp_modtype id args =
+  let fs = Summary.freeze_summaries () in
+  let env = Global.env () in
+  let env,arg_entries_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[]) 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 mbids = List.map fst arg_entries in
+  openmodtype_info := mbids;
+  let prefix = Lib.start_modtype id mp fs in
+  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
+  Lib.add_frozen_state ()
 
 
 let end_modtype id =
@@ -566,31 +592,38 @@ let end_modtype id =
   Lib.add_frozen_state ()(* to prevent recaching *)
 
 
-let declare_modtype id mte = 
-  let substobjs = get_modtype_substobjs mte in
-    ignore (add_leaf id (in_modtype (Some mte, substobjs)))
+let declare_modtype interp_modtype id args mty = 
+  let fs = Summary.freeze_summaries () in
+  let env = Global.env () in
+  let env,arg_entries_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  in
+  let arg_entries = List.concat (List.rev arg_entries_revlist) in
+  let base_mty = interp_modtype env mty in
+  let entry = 
+    List.fold_right 
+      (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+      arg_entries
+      base_mty
+  in
+  let substobjs = get_modtype_substobjs entry in
+  Summary.unfreeze_summaries fs;
+    
+  ignore (add_leaf id (in_modtype (Some entry, substobjs)))
 			       
 
 
-let rec get_module_substobjs locals = function
-    MEident (MPbound mbid as mp) -> 
-      begin
-	try 
-	  let mty = List.assoc mbid locals in
-	    get_modtype_substobjs mty
-	with
-	    Not_found -> MPmap.find mp !modtab_substobjs 
-      end
+let rec get_module_substobjs = function
   | MEident mp -> MPmap.find mp !modtab_substobjs 
   | MEfunctor (mbid,mty,mexpr) ->
       let (subst, mbids, msid, objs) = 
-	get_module_substobjs ((mbid,mty)::locals) mexpr 
+	get_module_substobjs mexpr 
       in
 	(subst, mbid::mbids, msid, objs)
   | MEstruct (msid,_) ->
       (empty_subst, [], msid, [])
   | MEapply (mexpr, MEident mp) ->
-      let (subst, mbids, msid, objs) = get_module_substobjs locals mexpr in
+      let (subst, mbids, msid, objs) = get_module_substobjs mexpr in
 	(match mbids with
 	   | mbid::mbids ->
 	       (add_mbid mbid mp subst, mbids, msid, objs)
@@ -599,18 +632,44 @@ let rec get_module_substobjs locals = function
       Modops.error_application_to_not_path mexpr
 
 
-let declare_module id me =
+let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
+
+  let fs = Summary.freeze_summaries () in
+  let env = Global.env () in
+  let env,arg_entries_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  in
+  let arg_entries = List.concat (List.rev arg_entries_revlist) in
+  let mty_entry_o = option_app (interp_modtype env) mty_o in
+  let mexpr_entry_o = option_app (interp_modexpr env) mexpr_o in
+  let entry = 
+    {mod_entry_type = 	    
+       option_app
+	 (List.fold_right 
+	    (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+	    arg_entries)
+	 mty_entry_o;
+     mod_entry_expr = 
+       option_app
+	 (List.fold_right 
+	    (fun (mbid,mte) me -> MEfunctor(mbid,mte,me))
+	    arg_entries)
+	 mexpr_entry_o }
+  in
   let substobjs =
-    match me with
+    match entry with
       | {mod_entry_type = Some mte} -> get_modtype_substobjs mte
-      | {mod_entry_expr = Some mexpr} -> get_module_substobjs [] mexpr
+      | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr
       | _ -> anomaly "declare_module: No type, no body ..."
   in
+  Summary.unfreeze_summaries fs;
+
   let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
   let substituted = subst_substobjs dir mp substobjs in
-    ignore (add_leaf
-	      id
-	      (in_module (Some me, substobjs, substituted)))
+
+  ignore (add_leaf
+	    id
+	    (in_module (Some entry, substobjs, substituted)))
 
 
 (*s Iterators. *)
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 17db827e8..5c228d161 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -11,6 +11,7 @@
 (*i*)
 open Names
 open Entries
+open Environ
 open Libnames
 open Libobject
 open Lib
@@ -22,22 +23,32 @@ open Lib
 
 (*s Modules *)
 
-val declare_module : identifier -> module_entry -> unit
+val declare_module : 
+  (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) ->
+  identifier -> 
+  (identifier list * 'modtype) list -> 'modtype option -> 'modexpr option -> unit
+
+val start_module : (env -> 'modtype -> module_type_entry) ->
+  identifier -> (identifier list * 'modtype) list -> 'modtype option -> unit
+
+(*val declare_module : identifier -> module_entry -> unit
 
 val start_module : 
   identifier -> identifier list -> (mod_bound_id * module_type_entry) list 
     -> module_type_entry option -> unit
+*)
 val end_module : identifier -> unit
 
 
 
 (*s Module types *)
 
-val declare_modtype : identifier -> module_type_entry -> unit
+val declare_modtype : (env -> 'modtype -> module_type_entry) -> 
+  identifier -> (identifier list * 'modtype) list -> 'modtype -> unit
+
+val start_modtype : (env -> 'modtype -> module_type_entry) -> 
+  identifier -> (identifier list * 'modtype) list -> unit
 
-val start_modtype : 
-  identifier -> identifier list -> (mod_bound_id * module_type_entry) list 
-    -> unit
 val end_modtype : identifier -> unit
 
 
diff --git a/parsing/astmod.ml b/parsing/astmod.ml
index 9c0915a4f..cbb19fa0b 100644
--- a/parsing/astmod.ml
+++ b/parsing/astmod.ml
@@ -65,31 +65,13 @@ let lookup_qualid (modtype:bool) qid =
    and the basename. Searches Nametab otherwise.
 *)
 
-let lookup_module binders qid =
-  try
-    let dir,id = repr_qualid qid in
-      (* dirpath in natural order *)
-    let idl = List.rev (id::repr_dirpath dir) in
-    let top_mp = MPbound (fst (List.assoc (List.hd idl) binders)) in
-      make_mp top_mp (List.tl idl)
-  with 
-      Not_found -> Nametab.locate_module qid
+let lookup_module qid =
+  Nametab.locate_module qid
 	
-let lookup_modtype binders qid =
-  try
-    let dir,id = repr_qualid qid in
-      (* dirpath in natural order *)
-    match List.rev (repr_dirpath dir) with
-      | hd::tl ->
-	  let top_mp = MPbound (fst (List.assoc hd binders)) in
-	  let mp = make_mp top_mp tl in
-	    make_kn mp empty_dirpath (label_of_id id)
-      | [] -> raise Not_found 
-	  (* may-be a module, but not a module type!*)
-  with
-      Not_found -> Nametab.locate_modtype qid
+let lookup_modtype qid =
+  Nametab.locate_modtype qid
 
-let transl_with_decl binders = function 
+let transl_with_decl env = function 
   | Node(loc,"WITHMODULE",[id_ast;qid_ast]) ->
       let id = match id_ast with
 	  Nvar(_,id) -> id
@@ -100,22 +82,22 @@ let transl_with_decl binders = function
   	    interp_qualid astl
 	| _ -> anomaly "QUALID expected"
       in
-	With_Module (id,lookup_module binders qid)
+	With_Module (id,lookup_module qid)
   | Node(loc,"WITHDEFINITION",[id_ast;cast]) ->
       let id = match id_ast with
 	  Nvar(_,id) -> id
 	| _ -> anomaly "Identifier AST expected"
       in
-      let c = interp_constr Evd.empty (Global.env()) cast in
+      let c = interp_constr Evd.empty env cast in
 	With_Definition (id,c)
   | _ -> anomaly "Unexpected AST"
 
-let rec transl_modtype binders = function 
+let rec interp_modtype env = function 
   | Node(loc,"MODTYPEQID",qid_ast) -> begin match qid_ast with 
       | [Node (loc, "QUALID", astl)] -> 
   	  let qid = interp_qualid astl in begin
 	      try 
-	        MTEident (lookup_modtype binders qid)
+	        MTEident (lookup_modtype qid)
 	      with
 	        | Not_found -> 
 		    Modops.error_not_a_modtype (*loc*) (string_of_qualid qid)
@@ -123,32 +105,18 @@ let rec transl_modtype binders = function
       | _ -> anomaly "QUALID expected"
     end
   | Node(loc,"MODTYPEWITH",[mty_ast;decl_ast]) ->
-      let mty = transl_modtype binders mty_ast in
-      let decl = transl_with_decl binders decl_ast in
+      let mty = interp_modtype env mty_ast in
+      let decl = transl_with_decl env decl_ast in
 	MTEwith(mty,decl)
   | _ -> anomaly "TODO: transl_modtype: I can handle qualid module types only"
  
 
-let transl_binder binders (idl,mty_ast) =
-  let mte = transl_modtype binders mty_ast in
-  let add_one binders id = 
-    if List.mem_assoc id binders then
-      error "Two identical module binders..."
-    else
-      let mbid = make_mbid (Lib.module_dp()) (string_of_id id) in
-	(id,(mbid,mte))::binders
-  in
-    List.fold_left add_one binders idl 
-
-let transl_binders = List.fold_left transl_binder
-
-
-let rec transl_modexpr binders = function 
+let rec interp_modexpr env = function 
   | Node(loc,"MODEXPRQID",qid_ast) -> begin match qid_ast with 
       | [Node (loc, "QUALID", astl)] -> 
 	  let qid = interp_qualid astl in begin
 	    try 
-	      MEident (lookup_module binders qid)
+	      MEident (lookup_module qid)
 	    with
 	      | Not_found -> 
 		 Modops.error_not_a_module (*loc*) (string_of_qualid qid)
@@ -156,17 +124,10 @@ let rec transl_modexpr binders = function
       | _ -> anomaly "QUALID expected"
     end
   | Node(_,"MODEXPRAPP",[ast1;ast2]) ->
-      let me1 = transl_modexpr binders ast1 in
-      let me2 = transl_modexpr binders ast2 in
+      let me1 = interp_modexpr env ast1 in
+      let me2 = interp_modexpr env ast2 in
 	MEapply(me1,me2)
   | Node(_,"MODEXPRAPP",_) -> 
       anomaly "transl_modexpr: MODEXPRAPP must have two arguments"
   | _ -> anomaly "transl_modexpr: I can handle MODEXPRQID or MODEXPRAPP only..."
 
-
-let interp_module_decl evd env args_ast mty_ast_o mexpr_ast_o = 
-  let binders = transl_binders [] args_ast in
-  let mty_o = option_app (transl_modtype binders) mty_ast_o in
-  let mexpr_o = option_app (transl_modexpr binders) mexpr_ast_o in
-    (List.rev binders, mty_o, mexpr_o)
-
diff --git a/parsing/astmod.mli b/parsing/astmod.mli
index 158f40e89..49e061a0b 100644
--- a/parsing/astmod.mli
+++ b/parsing/astmod.mli
@@ -19,12 +19,7 @@ open Evd
 (* Module expressions and module types are interpreted relatively to 
    eventual functor or funsig arguments. *)
 
-val interp_module_decl : evar_map -> env -> 
-  (identifier list * Coqast.t) list -> 
-  Coqast.t option ->
-  Coqast.t option
-    ->
-      (identifier * (mod_bound_id * module_type_entry)) list * 
-      module_type_entry option *
-      module_expr option
+val interp_modtype : env -> Coqast.t -> module_type_entry
+
+val interp_modexpr : env -> Coqast.t -> module_expr
 
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 075fdb03d..2b75049b2 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -13,44 +13,66 @@ open Declarations
 open Nameops
 open Libnames
 
-let print_modpath env mp = 
+let get_new_id locals id = 
+  let rec get_id l id = 
+    let dir = make_dirpath [id] in
+      if not (Nametab.exists_module dir) then
+	id
+      else
+	get_id (id::l) (Nameops.next_ident_away id l)
+  in
+    get_id (List.map snd locals) id
+
+let rec print_local_modpath locals = function
+  | MPbound mbid -> pr_id (List.assoc mbid locals)
+  | MPdot(mp,l) ->
+      print_local_modpath locals mp ++ str "." ++ pr_lab l
+  | MPself _ | MPfile _ -> raise Not_found
+
+let print_modpath locals mp = 
   try (* must be with let because streams are lazy! *)
-    let qid = Nametab.shortest_qualid_of_module mp in pr_qualid qid
+    let qid = Nametab.shortest_qualid_of_module mp in 
+      pr_qualid qid
   with
-    | Not_found as e -> 
-	match mp with 
-	  | MPbound mbid -> Nameops.pr_id (id_of_mbid mbid)
-	  | _ -> raise e
+    | Not_found -> print_local_modpath locals mp
 
-let print_kn env kn = 
-  let qid = Nametab.shortest_qualid_of_modtype kn in 
-    pr_qualid qid
+let print_kn locals kn = 
+  try
+    let qid = Nametab.shortest_qualid_of_modtype kn in 
+      pr_qualid qid
+  with
+      Not_found -> 
+	let (mp,_,l) = repr_kn kn in
+	  print_local_modpath locals mp ++ str"." ++ pr_lab l
 
 let rec flatten_app mexpr l = match mexpr with
   | MEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l)
   | mexpr -> mexpr::l
 
-let rec print_module name env with_body mb =
+let rec print_module name locals with_body mb =
   let body = match mb.mod_equiv, with_body, mb.mod_expr with 
     | None, false, _ 
     | None, true, None -> mt()
-    | None, true, Some mexpr -> str " := " ++ print_modexpr env mexpr
-    | Some mp, _, _ -> str " == " ++ print_modpath env mp
+    | None, true, Some mexpr -> 
+	spc () ++ str ":= " ++ print_modexpr locals mexpr
+    | Some mp, _, _ -> str " == " ++ print_modpath locals mp
   in
-  str "Module " ++ name ++ str" : " ++ print_modtype env mb.mod_type ++ body
+  hv 2 (str "Module " ++ name ++ spc () ++ str": " ++ 
+	print_modtype locals mb.mod_type ++ body)
 
-and print_modtype env mty = match mty with
-  | MTBident kn -> print_kn env kn
+and print_modtype locals mty = match mty with
+  | MTBident kn -> print_kn locals kn
   | MTBfunsig (mbid,mtb1,mtb2) ->
-(*      let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
-      in *)
+(*    let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
+      in *) 
+      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
       hov 2 (str "Funsig" ++ spc () ++ str "(" ++ 
-        pr_id (id_of_mbid mbid) ++ str " : " ++ print_modtype env mtb1 ++ 
-      str ")" ++ spc() ++ print_modtype env mtb2)
+        pr_id (id_of_mbid mbid) ++ str " : " ++ print_modtype locals mtb1 ++ 
+      str ")" ++ spc() ++ print_modtype locals' mtb2)
   | MTBsig (msid,sign) -> 
-      hv 2 (str "Sig" ++ spc () ++ print_sig env msid sign ++ brk (1,-2) ++ str "End")
+      hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End")
 
-and print_sig env msid sign = 
+and print_sig locals msid sign = 
   let print_spec (l,spec) = (match spec with
     | SPBconst _ -> str "Definition "
     | SPBmind _ -> str "Inductive "
@@ -59,7 +81,7 @@ and print_sig env msid sign =
   in
     prlist_with_sep spc print_spec sign
 
-and print_struct env msid struc = 
+and print_struct locals msid struc = 
   let print_body (l,body) = (match body with
     | SEBconst _ -> str "Definition "
     | SEBmind _ -> str "Inductive "
@@ -68,29 +90,28 @@ and print_struct env msid struc =
   in
     prlist_with_sep spc print_body struc
 
-and print_modexpr env mexpr = match mexpr with 
-  | MEBident mp -> print_modpath env mp
+and print_modexpr locals mexpr = match mexpr with 
+  | MEBident mp -> print_modpath locals mp
   | MEBfunctor (mbid,mty,mexpr) ->
-(*      let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
+(*    let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
       in *)
+      let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
       hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ 
-	     str ":" ++ print_modtype env mty ++ 
-      str "]" ++ spc () ++ print_modexpr env mexpr)
+	     str ":" ++ print_modtype locals mty ++ 
+      str "]" ++ spc () ++ print_modexpr locals' mexpr)
   | MEBstruct (msid, struc) -> 
-      hv 2 (str "Struct" ++ spc () ++ print_struct env msid struc ++ brk (1,-2) ++ str "End")
+      hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End")
   | MEBapply (mexpr,marg,_) -> 
       let lapp = flatten_app mexpr [marg] in
-	hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr env) lapp ++ str")")
+	hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")")
 
 
 
 let print_module with_body mp = 
-  let env = Global.env() in
-  let name = print_modpath env mp in
-    print_module name env with_body (Environ.lookup_module mp env) ++ fnl ()
+  let name = print_modpath [] mp in
+    print_module name [] with_body (Global.lookup_module mp) ++ fnl ()
 
 let print_modtype kn = 
-  let env = Global.env() in
-  let name = print_kn env kn in
-    str "Module Type " ++ name ++ str " = " ++
-    print_modtype env (Environ.lookup_modtype kn env) ++ fnl ()
+  let name = print_kn [] kn in
+    str "Module Type " ++ name ++ str " = " ++ 
+      print_modtype [] (Global.lookup_modtype kn) ++ fnl ()
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 904db670f..81e08d667 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -391,52 +391,30 @@ let vernac_scheme = build_scheme
 (**********************)
 (* Modules            *)
 
-let vernac_declare_module id bl mty_ast_o mexpr_ast_o = 
-  let evd = Evd.empty in
-  let env = Global.env () in
-  let arglist,base_mty_o,base_mexpr_o =
-    Astmod.interp_module_decl evd env bl mty_ast_o mexpr_ast_o 
-  in
-  let argids, args = List.split arglist 
-  in (* We check the state of the system (in section, in module type)
-	and what module information is supplied *)
-    if Lib.sections_are_opened () then
-      error "Modules and Module Types are not allowed inside sections";
-
-    match Lib.is_specification (), base_mty_o, base_mexpr_o with
-      | _, None, None 
-      | false, _, None ->
-	  Declaremods.start_module id argids args base_mty_o;
-	  if_verbose message 
-	    ("Interactive Module "^ string_of_id id ^" started")
+let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o = 
+  (* We check the state of the system (in section, in module type)
+     and what module information is supplied *)
+  if Lib.sections_are_opened () then
+    error "Modules and Module Types are not allowed inside sections";
+  
+  match Lib.is_specification (), mty_ast_o, mexpr_ast_o with
+    | _, None, None 
+    | false, _, None ->
+	Declaremods.start_module Astmod.interp_modtype
+	  id binders_ast mty_ast_o;
+	if_verbose message 
+	  ("Interactive Module "^ string_of_id id ^" started")
 	  
-      | true, Some _, None
-      | true, _, Some (MEident _)
-      | false, _, Some _ ->
-	  let mexpr_o = 
-	    option_app
-	      (List.fold_right 
-		 (fun (mbid,mte) me -> MEfunctor(mbid,mte,me))
-		 args)
-	      base_mexpr_o
-	  in
-	  let mty_o = 
-	    option_app
-	      (List.fold_right 
-		 (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
-		 args)
-	      base_mty_o
-	  in
-	  let mod_entry = 
-	    {mod_entry_type = mty_o;
-	     mod_entry_expr = mexpr_o}
-	  in
-	    Declaremods.declare_module id mod_entry;
-	    if_verbose message 
-	      ("Module "^ string_of_id id ^" is defined")
-
-      | true, _, Some (MEfunctor _ | MEapply _ | MEstruct _) ->
-	  error "Module definition not allowed in a Module Type"
+    | true, Some _, None
+    | true, _, Some (Coqast.Node(_,"QUALID",_))
+    | false, _, Some _ ->
+	Declaremods.declare_module Astmod.interp_modtype Astmod.interp_modexpr
+	  id binders_ast mty_ast_o mexpr_ast_o;
+	if_verbose message 
+	  ("Module "^ string_of_id id ^" is defined")
+
+    | true, _, _ ->
+	error "Module definition not allowed in a Module Type"
 
 
 let vernac_end_module id =
@@ -446,33 +424,21 @@ let vernac_end_module id =
   
 
 
-let vernac_declare_module_type id bl mty_ast_o =
-  let evd = Evd.empty in
-  let env = Global.env () in
-  let arglist,base_mty_o,_ =
-    Astmod.interp_module_decl evd env bl mty_ast_o None
-  in
-  let argids, args = List.split arglist 
-  in 
-    if Lib.sections_are_opened () then
-      error "Modules and Module Types are not allowed inside sections";
-
-    match base_mty_o with
-      | None ->
-	  Declaremods.start_modtype id argids args;
-	  if_verbose message 
-	    ("Interactive Module Type "^ string_of_id id ^" started")
-
-      | Some base_mty ->
-	  let mty = 
-	    List.fold_right 
-	      (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
-	      args
-	      base_mty
-	  in
-	    Declaremods.declare_modtype id mty;
-	    if_verbose message 
-	      ("Module Type "^ string_of_id id ^" is defined")
+let vernac_declare_module_type id binders_ast mty_ast_o =
+  if Lib.sections_are_opened () then
+    error "Modules and Module Types are not allowed inside sections";
+  
+  match mty_ast_o with
+    | None ->
+	Declaremods.start_modtype Astmod.interp_modtype id binders_ast;
+	if_verbose message 
+	  ("Interactive Module Type "^ string_of_id id ^" started")
+	  
+    | Some base_mty ->
+	Declaremods.declare_modtype Astmod.interp_modtype 
+	  id binders_ast base_mty;
+	if_verbose message 
+	  ("Module Type "^ string_of_id id ^" is defined")
 
 
 let vernac_end_modtype id =