Petites corrections ici et la

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

3 files changed, 30 insertions, 14 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 76ed46619..7b5adfdc9 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -549,28 +549,38 @@ let declare_modtype id mte =
 			       
 
 
-let rec get_module_substobjs = function
-    MEident mp -> MPmap.find mp !modtab_substobjs 
-  | MEfunctor (mbid,_,mexpr) ->
-      let (subst, mbids, msid, objs) = get_module_substobjs mexpr in
+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
+  | MEident mp -> MPmap.find mp !modtab_substobjs 
+  | MEfunctor (mbid,mty,mexpr) ->
+      let (subst, mbids, msid, objs) = 
+	get_module_substobjs ((mbid,mty)::locals) mexpr 
+      in
 	(subst, mbid::mbids, msid, objs)
   | MEstruct (msid,_) ->
       (empty_subst, [], msid, [])
   | MEapply (mexpr, MEident mp) ->
-      let (subst, mbids, msid, objs) = get_module_substobjs mexpr in
+      let (subst, mbids, msid, objs) = get_module_substobjs locals mexpr in
 	(match mbids with
 	   | mbid::mbids ->
 	       (add_mbid mbid mp subst, mbids, msid, objs)
 	   | [] -> anomaly "Too few arguments in functor")
-  | MEapply (_,_) ->
-      anomaly "The argument of a module application must be a path!"
+  | MEapply (_,mexpr) ->
+      Modops.error_application_to_not_path mexpr
 
 
 let declare_module id me =
   let substobjs =
     match me 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
   let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
diff --git a/library/nametab.ml b/library/nametab.ml
index c80675aec..bc419a237 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -32,14 +32,14 @@ type 'a path_status = Nothing | Relative of 'a | Absolute of 'a
 (* Dictionaries of short names *)
 type 'a nametree = ('a path_status * 'a nametree ModIdmap.t)
 type ccitab = extended_global_reference nametree Idmap.t
-type kntab = kernel_name nametree Idmap.t
+type knsptab = (kernel_name * section_path) nametree Idmap.t
 type objtab = section_path nametree Idmap.t
 type dirtab = global_dir_reference nametree ModIdmap.t
 
 let the_ccitab = ref (Idmap.empty : ccitab)
 let the_dirtab = ref (ModIdmap.empty : dirtab)
 let the_objtab = ref (Idmap.empty : objtab)
-let the_modtypetab = ref (Idmap.empty : kntab)
+let the_modtypetab = ref (Idmap.empty : knsptab)
 
 (* This table translates extended_global_references back to section paths *)
 module Globtab = Map.Make(struct type t=extended_global_reference 
@@ -194,7 +194,7 @@ let push_syntactic_definition visibility sp kn =
 
 let push = push_cci
 
-let push_modtype = push_idtree the_modtypetab
+let push_modtype vis sp kn = push_idtree the_modtypetab vis sp (kn,sp)
 
 
 (* This is for dischargeable non-cci objects (removed at the end of the
@@ -257,7 +257,8 @@ let locate_syntactic_definition qid = match extended_locate qid with
   | TrueGlobal _ -> raise Not_found
   | SyntacticDef kn -> kn
 
-let locate_modtype qid = get (find_modtype qid)
+let full_name_modtype qid = get (find_modtype qid)
+let locate_modtype qid = fst (get (find_modtype qid))
 
 let locate_obj qid = get (find_in_idtree the_objtab qid)
 
@@ -376,24 +377,27 @@ let global_inductive (loc,qid as locqid) =
 (********************************************************************)
 (* Registration of tables as a global table and rollback            *)
 
-type frozen = ccitab * dirtab * objtab * globtab
+type frozen = ccitab * dirtab * objtab * knsptab * globtab
 
 let init () = 
   the_ccitab := Idmap.empty; 
   the_dirtab := ModIdmap.empty;
   the_objtab := Idmap.empty;
+  the_modtypetab := Idmap.empty;
   the_globtab := Globtab.empty
 
 let freeze () =
   !the_ccitab, 
   !the_dirtab,
   !the_objtab,
+  !the_modtypetab,
   !the_globtab
 
-let unfreeze (mc,md,mo,gt) =
+let unfreeze (mc,md,mo,mt,gt) =
   the_ccitab := mc;
   the_dirtab := md;
   the_objtab := mo;
+  the_modtypetab := mt;
   the_globtab := gt
 
 let _ = 
diff --git a/library/nametab.mli b/library/nametab.mli
index b64fe0d9d..626a529e6 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -120,6 +120,8 @@ val exists_dir : dir_path -> bool
 val exists_section : dir_path -> bool (* deprecated *)
 val exists_module : dir_path -> bool (* deprecated *)
 
+val full_name_modtype : qualid -> kernel_name * section_path
+
 (*s Roots of the space of absolute names *)
 
 (* This turns a "user" absolute name into a global reference;