Parsing

- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
  lieu de string)

Table des noms qualifiés

- Remplacement de la table de visibilité par une table qui ne cache
  plus les noms de modules et sections mais seulement les noms des
  constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
  module A déjà existant : seuls les noms de constructions de l'ancien
  A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
  constantes définies à l'intérieur de sections et simplification
  connexes (suppression de END-SECTION, une seule table de noms qui ne
  survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
  Require and co, tests de cohérence; pour être cohérent avec la non
  survie des tables de noms à la sortie des section, les require à
  l'intérieur d'une section eux aussi sont refaits à la fermeture de la
  section


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

11 files changed, 159 insertions, 213 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 1a3cc28008..6b0ed89ab4 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -37,7 +37,8 @@ let stre_gt = function
   | (_,NeverDischarge) -> true
   | (_,NotDeclare) -> true
   | (DischargeAt sp1,DischargeAt sp2) ->
-      dirpath_prefix_of sp1 sp2 (* was sp_gt but don't understand why - HH *)
+      is_dirpath_prefix_of sp1 sp2
+	(* was sp_gt but don't understand why - HH *)
 
 let stre_max (stre1,stre2) =
   if stre_gt (stre1,stre2) then stre1 else stre2
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0384ca8048..b3a34e2ce6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -28,9 +28,9 @@ open Proof_type
 open Tacmach
 
 let mkCastC(c,t) = ope("CAST",[c;t])
-let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)])
+let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some x,b)])
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
-let mkProdC (x,a,b) = ope("PROD",[a;slam(Some (string_of_id x),b)])
+let mkProdC (x,a,b) = ope("PROD",[a;slam(Some x,b)])
 let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
 
 (* Commands of the interface *)
@@ -102,13 +102,13 @@ let syntax_definition ident com =
 
 let parameter_def_var ident c =
   let c = interp_type Evd.empty (Global.env()) c in
-  let sp = declare_parameter (id_of_string ident) c in
-  if_verbose message (ident ^ " is assumed");
+  let sp = declare_parameter ident c in
+  if_verbose message ((string_of_id ident) ^ " is assumed");
   sp
 
 let declare_global_assumption ident c =
   let sp = parameter_def_var ident c in
-  wARNING [< 'sTR ident; 'sTR" is declared as a parameter";
+  wARNING [< pr_id ident; 'sTR" is declared as a parameter";
              'sTR" because it is at a global level" >];
   ConstRef sp
 
@@ -118,11 +118,10 @@ let hypothesis_def_var is_refining ident n c =
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
 	  let t = interp_type Evd.empty (Global.env()) c in
-          let sp = declare_variable (id_of_string ident)
-		     (SectionLocalAssum t,n,false) in
-	  if_verbose message (ident ^ " is assumed");
+          let sp = declare_variable ident (SectionLocalAssum t,n,false) in
+	  if_verbose message ((string_of_id ident) ^ " is assumed");
           if is_refining then 
-            mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
+            mSGERRNL [< 'sTR"Warning: Variable "; pr_id ident; 
                         'sTR" is not visible from current goals" >];
 	  VarRef sp
         end
@@ -437,7 +436,7 @@ let apply_tac_not_declare id pft = function
 let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
   strength =
   begin match strength with
-    | DischargeAt disch_sp when Lib.is_section_p disch_sp ->
+    | DischargeAt disch_sp when Lib.is_section_p disch_sp (*&& not opacity*) ->
 	let c = constr_of_constr_entry const in
 	let _ = declare_variable id (SectionLocalDef c,strength,opacity) in ()
     | NeverDischarge | DischargeAt _ ->
@@ -464,12 +463,12 @@ let check_anonymity id save_ident =
 let save_anonymous opacity save_ident =
   let id,(const,strength) = Pfedit.cook_proof () in
   check_anonymity id save_ident;
-  save opacity (id_of_string save_ident) const strength
+  save opacity save_ident const strength
 
 let save_anonymous_with_strength strength opacity save_ident =
   let id,(const,_) = Pfedit.cook_proof () in
   check_anonymity id save_ident;
-  save opacity (id_of_string save_ident) const strength
+  save opacity save_ident const strength
 
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b7b9d0f130..3c1d52b6a3 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -12,6 +12,7 @@
 open Names
 open Term
 open Declare
+open Library
 (*i*)
 
 (*s Declaration functions. The following functions take ASTs,
@@ -31,10 +32,10 @@ val syntax_definition : identifier -> Coqast.t -> unit
 val abstraction_definition : identifier -> int array -> Coqast.t -> unit
 i*)
 
-val hypothesis_def_var : bool -> string -> strength -> Coqast.t
+val hypothesis_def_var : bool -> identifier -> strength -> Coqast.t
   -> global_reference
 
-val parameter_def_var : string -> Coqast.t -> constant_path
+val parameter_def_var : identifier -> Coqast.t -> constant_path
 
 val build_mutual : 
   (identifier * Coqast.t) list -> 
@@ -61,13 +62,13 @@ val save_named : bool -> unit
 (* [save_anonymous b name] behaves as [save_named] but declares the theorem
 under the name [name] and respects the strength of the declaration *)
 
-val save_anonymous : bool -> string -> unit
+val save_anonymous : bool -> identifier -> unit
 
 (* [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
    declares the theorem under the name [name] and gives it the
    strength [strength] *)
 
-val save_anonymous_with_strength : strength -> bool -> string -> unit
+val save_anonymous_with_strength : strength -> bool -> identifier -> unit
 
 (* [get_current_context ()] returns the evar context and env of the
    current open proof if any, otherwise returns the empty evar context
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 80c81d243b..e7f56ef87a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -80,16 +80,19 @@ let init_load_path () =
   List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
   add_ml_include camlp4;
-  Mltop.add_path "." [Nametab.default_root];
+  Mltop.add_path "." Nametab.default_root_prefix;
   (* additional loadpath, given with -I -include -R options *)
   List.iter 
     (fun (s,alias,reci) ->
        if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias)
     (List.rev !includes)
 
+(* Must be done after restoring initial state! *)
 let init_library_roots () =
   List.iter
-    (fun (_,alias,_) -> Nametab.push_library_root (List.hd alias)) !includes;
+    (fun (_,alias,_) ->
+      if alias <> [] then Nametab.push_library_root (List.hd alias))
+    !includes;
   includes := []
 
 (* Initialises the Ocaml toplevel before launching it, so that it can
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a88223925f..7d293aed9a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -12,6 +12,7 @@ open Pp
 open Util
 open System
 open Options
+open Names
 open States
 open Toplevel
 open Coqinit
@@ -44,10 +45,10 @@ let outputstate = ref ""
 let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
-let set_include d p = push_include (d,Names.dirpath_of_string p)
-let set_rec_include d p = push_rec_include (d,Names.dirpath_of_string p)
-let set_default_include d = set_include d Nametab.default_root
-let set_default_rec_include d = set_rec_include d Nametab.default_root
+let set_include d p = push_include (d,p)
+let set_rec_include d p = push_rec_include (d,p)
+let set_default_include d = set_include d Nametab.default_root_prefix
+let set_default_rec_include d = set_rec_include d Nametab.default_root_prefix
  
 let load_vernacular_list = ref ([] : string list)
 let add_load_vernacular s =
@@ -60,15 +61,15 @@ let load_vernacular () =
 let load_vernacular_obj = ref ([] : string list)
 let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
 let load_vernac_obj () = 
-  List.iter
-    (fun s -> Library.load_module (Filename.basename s) (Some s))
-    (List.rev !load_vernacular_obj)
+  List.iter Library.read_module_from_file (List.rev !load_vernacular_obj)
 
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
 let require () =
   List.iter
-    (fun s -> Library.require_module None (Filename.basename s) (Some s) false)
+    (fun s -> 
+      let qid = Nametab.make_qualid [] (id_of_string (Filename.basename s)) in
+      Library.require_module None qid  (Some s) false)
     (List.rev !require_list)
 
 (* Re-exec Coq in bytecode or native code if necessary. [s] is either
@@ -110,7 +111,7 @@ let parse_args () =
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | "-R" :: d :: p :: rem -> set_rec_include d p; parse rem
+    | "-R" :: d :: p :: rem ->set_rec_include d (dirpath_of_string p);parse rem
     | "-R" :: ([] | [_]) -> usage ()
 
     | "-q" :: rem -> no_load_rc (); parse rem
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 2b3fd2c5d2..c8e031bb86 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -26,6 +26,7 @@ open Impargs
 open Classops
 open Class
 open Recordops
+open Library
 
 let recalc_sp dir sp =
   let (_,spid,k) = repr_path sp in Names.make_path dir spid k
@@ -169,6 +170,7 @@ type discharge_operation =
   | Struc of inductive_path * (unit -> struc_typ)
   | Objdef of constant_path
   | Coercion of coercion_entry
+  | Require of module_reference
 
 (* Main function to traverse the library segment and compute the various
    discharge operations. *)
@@ -179,8 +181,13 @@ let process_object oldenv dir sec_sp
   match tag with
     | "VARIABLE" ->
 	let ((id,c,t),stre,sticky) = get_variable sp in
-	if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then
+	(* VARIABLE means local (entry Variable/Hypothesis/Local and are *)
+	(* always discharged *)
+(*
+ 	if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then
+*)
 	  (ops,id::ids_to_discard,work_alist)
+(*
 	else
 	  let imp = is_implicit_var sp in
 	  let newdecl =
@@ -194,13 +201,19 @@ let process_object oldenv dir sec_sp
 	  in
 	  (Variable (id,newdecl,stre,sticky,imp) :: ops,
 	   ids_to_discard,work_alist)
+*)
 
     | "CONSTANT" | "PARAMETER" ->
-	let stre = constant_or_parameter_strength sp in
+	(* CONSTANT/PARAMETER means never discharge (though visibility *)
+	(* may vary) *)
+ 	let stre = constant_or_parameter_strength sp in
+(*
 	if stre = (DischargeAt sec_sp) then
-	  let constl = (sp, DO_REPLACE)::constl in
+	  let cb = Environ.lookup_constant sp oldenv in
+	  let constl = (sp, DO_REPLACE cb)::constl in
 	  (ops, ids_to_discard, (constl,indl,cstrl))
 	else
+*)
 	  let cb = Environ.lookup_constant sp oldenv in
 	  let spid = basename sp in
 	  let imp = is_implicit_constant sp in
@@ -209,7 +222,7 @@ let process_object oldenv dir sec_sp
 	    let modl = build_abstract_list cb.const_hyps ids_to_discard in
 	    [ (sp, DO_ABSTRACT(newsp,modl)) ]
 	  in
-	  let r = { d_from = sp;
+	  let r = { d_from = cb;
 		    d_modlist = work_alist;
 		    d_abstract = ids_to_discard } in
 	  let op = Constant (spid,r,stre,cb.const_opaque,imp) in
@@ -255,6 +268,10 @@ let process_object oldenv dir sec_sp
 	let new_sp = recalc_sp dir sp in
         ((Objdef new_sp)::ops, ids_to_discard, work_alist)
 
+    | "REQUIRE" -> 
+	let c = out_require lobj in
+	((Require c)::ops, ids_to_discard, work_alist)
+
     | _ -> (ops,ids_to_discard,work_alist)
 
 let process_item oldenv dir sec_sp acc = function
@@ -284,79 +301,18 @@ let process_operation = function
   | Objdef newsp ->
       begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end
   | Coercion y -> add_new_coercion y
+  | Require y -> reload_module y
 
-let push_inductive_names ccitab sp mie =
-  let _,ccitab =
-    List.fold_left
-      (fun (n,ccitab) ind ->
-	 let id = ind.mind_entry_typename in
-	 let indsp = (sp,n) in
-	 let _,ccitab =
-	   List.fold_left
-	     (fun (p,ccitab) x ->
-		(p+1, Idmap.add x (ConstructRef (indsp,p)) ccitab))
-	     (1,Idmap.add id (IndRef indsp) ccitab)
-	     ind.mind_entry_consnames in
-	 (n+1,ccitab))
-      (0,ccitab)
-      mie.mind_entry_inds
-  in ccitab
-
-(*s Operations performed at section closing. *)
-
-let cache_end_section (_,(sp,mc)) =
-  Nametab.push_section sp mc;
-  Nametab.open_section_contents (Nametab.qualid_of_sp sp)
-
-let load_end_section (_,(sp,mc)) =
-  Nametab.push_module sp mc
-
-let open_end_section (_,(sp,_)) =
-  Nametab.rec_open_module_contents (Nametab.qualid_of_sp sp)
-
-let (in_end_section, out_end_section) =
-  declare_object
-    ("END-SECTION",
-     { cache_function = cache_end_section;
-       load_function = load_end_section;
-       open_function = open_end_section;
-       export_function = (fun x -> Some x) })
-
-let rec process_object (ccitab, objtab, modtab as tabs) = function
-  | sp,Leaf obj -> 
-      begin match object_tag obj with
-	| "CONSTANT" | "PARAMETER" ->
-            (Idmap.add (basename sp) (ConstRef sp) ccitab,objtab,modtab)
-	| "INDUCTIVE" ->
-	    let mie = out_inductive obj in
-	    (push_inductive_names ccitab sp mie, objtab, modtab)
-        (* Variables are never visible *)
-	| "VARIABLE" -> tabs
-	| "END-SECTION" ->
-	    let (sp,mc) = out_end_section obj in
-	    let id = string_of_id (basename sp) in
-	    (ccitab, objtab, Stringmap.add id (sp,mc) modtab)
-        (* All the rest is visible only at toplevel ??? *)
-        (* Actually it is unsafe, it should be visible only in empty context *)
-        (* ou quelque chose comme cela *)
-	| "CLASS" | "COERCION" | "STRUCTURE" | "OBJDEF1" | "SYNTAXCONSTANT"
-	| _ ->
-	    (ccitab, Idmap.add (basename sp) (sp,obj) objtab, modtab)
-      end 
-  | _,(ClosedSection _ | OpenedSection _ | FrozenState _ | Module _) ->  tabs
-
-and segment_contents seg =
-  let ccitab, objtab, modtab =
-    List.fold_left process_object
-      (Idmap.empty, Idmap.empty, Stringmap.empty)
-      seg
-  in 
-  Nametab.Closed (ccitab, objtab, modtab)
+let catch_not_found f x =
+  try f x
+  with Not_found ->
+    error ("Something is missing; perhaps a reference to a"^
+    " module required inside the section")
 
 let close_section _ s = 
   let oldenv = Global.env() in
   let sec_sp,decls,fs = close_section false s in
-  let newdir = dirpath (* Trick for HELM *) sec_sp in
+  let newdir = dirpath sec_sp in
   let olddir = wd_of_sp sec_sp in
   let (ops,ids,_) = 
     if Options.immediate_discharge then ([],[],([],[],[]))
@@ -367,14 +323,8 @@ let close_section _ s =
   let ids = last_section_hyps olddir in
   Global.pop_named_decls ids;
   Summary.unfreeze_lost_summaries fs;
-  let mc = segment_contents decls in
-  add_anonymous_leaf (in_end_section (sec_sp,mc));
   add_frozen_state ();
   if Options.immediate_discharge then ()
   else
-    List.iter process_operation (List.rev ops)
-
-let save_module_to s f =
-  Library.save_module_to segment_contents s f
-
-
+    catch_not_found (List.iter process_operation) (List.rev ops);
+  Nametab.push_section olddir
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 2f7b247ac3..42ac9d790e 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -8,11 +8,11 @@
 
 (*i $Id$ i*)
 
+open Names
+
 (* This module implements the discharge mechanism. It provides a function to
    close the last opened section. That function calls [Lib.close_section] and
    then re-introduce all the discharged versions of the objects that were
    defined in the section. *)
 
-val close_section : bool -> string -> unit
-
-val save_module_to : string -> string -> unit
+val close_section : bool -> identifier -> unit
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 0499eff838..51271b510d 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -35,7 +35,7 @@ open Vernacinterp
    Finally, we can create an object which is an ML module, and require
    that the "caching" of the ML module cause the loading of the
    associated ML file, if that file has not been yet loaded.  Of
-   course, the problem is how to record dependences between ML
+   course, the problem is how to record dependencies between ML
    modules.
    (I do not know of a solution to this problem, other than to
    put all the needed names into the ML Module object.) *)
@@ -44,8 +44,7 @@ open Vernacinterp
 let coq_mlpath_copy = ref []
 let keep_copy_mlpath s = 
   let dir = glob s in
-  let lpe = { directory = dir; coq_dirpath = [] } in
-  coq_mlpath_copy := lpe :: !coq_mlpath_copy
+  coq_mlpath_copy := dir :: !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
 type toplevel = { 
@@ -144,33 +143,33 @@ let add_ml_dir s =
 
 (* For Rec Add ML Path *)
 let add_rec_ml_dir dir = 
-  List.iter (fun lpe -> add_ml_dir lpe.directory) (all_subdirs dir None)
+  List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs dir)
 
 (* Adding files to Coq and ML loadpath *)
 
 let add_path dir coq_dirpath =
-  if coq_dirpath = [] then anomaly "add_path: empty path in library";
   if exists_dir dir then
     begin
       add_ml_dir dir;
-      Library.add_load_path_entry
-	{ directory = dir; coq_dirpath = coq_dirpath };
-      Nametab.push_library_root (List.hd coq_dirpath)
+      Library.add_load_path_entry (dir,coq_dirpath);
+      if coq_dirpath <> [] then Nametab.push_library_root (List.hd coq_dirpath)
     end
   else
     wARNING [< 'sTR ("Cannot open " ^ dir) >]
 
 let add_rec_path dir coq_dirpath =
-  if coq_dirpath = [] then anomaly "add_path: empty path in library";
-  let dirs = all_subdirs dir (Some coq_dirpath) in
+  let dirs = all_subdirs dir in
   if dirs <> [] then
+    let convert = List.map Names.id_of_string in
+    let dirs = List.map (fun (lp,cp) -> (lp,coq_dirpath@(convert cp))) dirs in
     begin
-      List.iter (fun lpe -> add_ml_dir lpe.directory) dirs;
+      List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
       List.iter Library.add_load_path_entry dirs;
-      Nametab.push_library_root (List.hd coq_dirpath)
+      if coq_dirpath <> [] then Nametab.push_library_root (List.hd coq_dirpath)
+      else List.iter (fun (_, cp) -> Nametab.push_library_root (List.hd cp)) dirs
     end
-    else
-      wARNING [< 'sTR ("Cannot open " ^ dir) >]
+  else
+    wARNING [< 'sTR ("Cannot open " ^ dir) >]
 
 (* convertit un nom quelconque en nom de fichier ou de module *) 
 let mod_of_name name =
@@ -284,11 +283,11 @@ let declare_ml_modules l =
 let print_ml_path () =
   let l = !coq_mlpath_copy in
   pPNL [< 'sTR"ML Load Path:"; 'fNL; 'sTR"  ";
-          hV 0 (prlist_with_sep pr_fnl (fun e -> [< 'sTR e.directory >]) l) >]
+          hV 0 (prlist_with_sep pr_fnl pr_str l) >]
 
 	  (* Printing of loaded ML modules *)
 	  
 let print_ml_modules () =
   let l = get_loaded_modules () in
   pP [< 'sTR"Loaded ML Modules : " ;
-        hOV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l); 'fNL >]
+        hOV 0 (prlist_with_sep pr_fnl pr_str l); 'fNL >]
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 5df670982c..13b2891ecf 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -24,20 +24,17 @@ open Command
 let make_constructor idstruc idps fields  =
   let app_constructor = 
     Ast.ope("APPLISTEXPL",
-        (Ast.nvar (string_of_id idstruc))::
-        List.map (fun id -> Ast.nvar(string_of_id id)) idps) in
+        (Ast.nvar idstruc):: List.map (fun id -> Ast.nvar id) idps) in
   let rec aux fields =
     match fields with
       | [] -> app_constructor
-      | (id,true,ty)::l ->
-	  Ast.ope("PROD",[ty; Ast.slam(Some (string_of_id id), aux l)])
-      | (id,false,c)::l ->
-	  Ast.ope("LETIN",[c; Ast.slam(Some (string_of_id id), aux l)])
+      | (id,true,ty)::l -> Ast.ope("PROD",[ty; Ast.slam(Some id, aux l)])
+      | (id,false,c)::l -> Ast.ope("LETIN",[c; Ast.slam(Some id, aux l)])
   in 
   aux fields
 
 let occur_fields id fs =
-  List.exists (fun (_,_,a) -> Ast.occur_var_ast (string_of_id id) a) fs
+  List.exists (fun (_,_,a) -> Ast.occur_var_ast id a) fs
 
 let interp_decl sigma env (id,assum,t) =
   if assum then
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d36779b43d..82d31cf641 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -143,11 +143,11 @@ let print_located_qualid qid =
   with Not_found ->
     error ((Nametab.string_of_qualid qid) ^ " not a defined object")
 
-let print_path_entry s =
-  [< 'sTR s.directory; 'tBRK (0,2); 'sTR (string_of_dirpath s.coq_dirpath) >]
+let print_path_entry (s,l) =
+  [< 'sTR s; 'tBRK (0,2); 'sTR (string_of_dirpath l) >]
 
 let print_loadpath () =
-  let l = Library.get_load_path () in
+  let l = Library.get_full_load_path () in
   mSGNL (Pp.t [< 'sTR "Physical path:                                 ";
 		 'tAB; 'sTR "Logical Path:"; 'fNL; 
 		 prlist_with_sep pr_fnl print_path_entry l >])
@@ -169,11 +169,29 @@ let _ =
        | [VARG_STRING f] -> (fun () -> locate_file f)
        | _ -> bad_vernac_args "LocateFile")
 
+let msg_found_library = function
+  | Library.LibLoaded, fulldir, file ->
+      mSG [< pr_dirpath fulldir; 'sTR " has been loaded from file"; 'fNL;
+      'sTR file; 'fNL >]
+  | Library.LibInPath, fulldir, file ->
+      mSG [< pr_dirpath fulldir; 'sTR " is bound to file "; 'sTR file; 'fNL >]
+
+let msg_notfound_library qid = function
+  | Library.LibUnmappedDir ->
+      let dir = fst (Nametab.repr_qualid qid) in
+      mSG [< 'sTR "No physical path is bound to "; pr_dirpath dir; 'fNL >]
+  | Library.LibNotFound ->
+      mSG (hOV 0 
+	[< 'sTR"Unable to locate library"; 'sPC; Nametab.pr_qualid qid; 'fNL >])
+  | _ -> assert false
+
 let _ = 
   add "LocateLibrary"
     (function 
-       | [VARG_IDENTIFIER id] ->
-	   (fun () -> locate_file ((string_of_id id)^".vo"))
+       | [VARG_QUALID qid] ->
+	   (fun () ->
+	     try msg_found_library (Library.locate_qualified_library qid)
+	     with e -> msg_notfound_library qid e)
        | _ -> bad_vernac_args "LocateLibrary")
 
 let _ = 
@@ -187,10 +205,10 @@ let _ =
   add "ADDPATH"
     (function 
        | [VARG_STRING dir] ->
-	   (fun () -> Mltop.add_path dir [Nametab.default_root])
+	   (fun () -> Mltop.add_path dir Nametab.default_root_prefix)
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = Nametab.repr_qualid alias in
-	    (fun () -> Mltop.add_path dir (aliasdir@[string_of_id aliasname]))
+	   (fun () -> Mltop.add_path dir (aliasdir@[aliasname]))
        | _ -> bad_vernac_args "ADDPATH")
 
 (* For compatibility *)
@@ -204,13 +222,10 @@ let _ =
   add "RECADDPATH"
     (function 
        | [VARG_STRING dir] ->
-	   (fun () -> Mltop.add_rec_path dir [Nametab.default_root])
+	   (fun () -> Mltop.add_rec_path dir Nametab.default_root_prefix)
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = Nametab.repr_qualid alias in
-	    (fun () ->
-	       let alias = aliasdir@[string_of_id aliasname] in
-	       Mltop.add_rec_path dir alias;
-	       Nametab.push_library_root (List.hd alias))
+	    (fun () -> Mltop.add_rec_path dir (aliasdir@[aliasname]))
        | _ -> bad_vernac_args "RECADDPATH")
 
 (* For compatibility *)
@@ -316,34 +331,37 @@ let _ =
     (function 
        | [VARG_IDENTIFIER id] ->
 	   let s = string_of_id id in
-	   let lpe,_ = 
-	     System.find_file_in_path (Library.get_load_path ()) (s^".v") in
-	   fun () -> Lib.start_module (lpe.coq_dirpath @ [s])
+	   let lpe,_ = System.find_file_in_path (Library.get_load_path ()) (s^".v") in
+	   let dir = (Library.find_logical_path lpe) @ [id] in
+	   fun () ->
+	     Lib.start_module dir
        | _ -> bad_vernac_args "BeginModule")
 
 let _ =
   add "WriteModule"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   fun () -> let m = string_of_id id in Discharge.save_module_to m m
+	   let mid = Lib.end_module id in
+	   fun () -> let m = string_of_id id in Library.save_module_to mid m
        | [VARG_IDENTIFIER id; VARG_STRING f] ->
-	   fun () -> Discharge.save_module_to (string_of_id id) f
+	   let mid = Lib.end_module id in
+	   fun () -> Library.save_module_to mid f
        | _ -> bad_vernac_args "WriteModule")
 
 let _ =
   add "ReadModule"
     (function 
-       | [VARG_IDENTIFIER id] ->
-	   fun () -> 
-	     without_mes_ambig Library.load_module (string_of_id id) None
+       | [VARG_QUALID qid] ->
+	   fun () -> without_mes_ambig Library.read_module qid
        | _ -> bad_vernac_args "ReadModule")
 
 let _ =
   add "ImportModule"
     (function 
-       | [VARG_IDENTIFIER id] ->
-	   fun () -> 
-	     without_mes_ambig Library.import_module (string_of_id id)
+       | [VARG_QUALID qid] ->
+	   fun () ->
+	     let fullname = Nametab.locate_loaded_library qid in 
+	     without_mes_ambig Library.import_module fullname
        | _ -> bad_vernac_args "ImportModule")
 
 let _ =
@@ -354,12 +372,10 @@ let _ =
               let opened = Library.opened_modules ()
 	      and loaded = Library.loaded_modules () in
               mSG [< 'sTR"Loaded Modules: ";
-		     hOV 0 (prlist_with_sep pr_fnl 
-			      (fun s -> [< 'sTR s >]) loaded);
+		     hOV 0 (prlist_with_sep pr_fnl pr_dirpath loaded);
 		     'fNL;
 		     'sTR"Imported (open) Modules: ";
-		     hOV 0 (prlist_with_sep pr_fnl
-			      (fun s -> [< 'sTR s >]) opened); 
+		     hOV 0 (prlist_with_sep pr_fnl pr_dirpath opened); 
 		     'fNL >])
        | _ -> bad_vernac_args "PrintModules")
 
@@ -369,7 +385,7 @@ let _ =
   add "BeginSection"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   (fun () -> let _ = Lib.open_section (string_of_id id) in ())
+	   (fun () -> let _ = Lib.open_section id in ())
        | _ -> bad_vernac_args "BeginSection")
 
 let _ =
@@ -378,7 +394,7 @@ let _ =
        | [VARG_IDENTIFIER id] ->
 	   (fun () ->
 	      check_no_pending_proofs ();
-              Discharge.close_section (is_verbose ()) (string_of_id id))
+              Discharge.close_section (is_verbose ()) id)
        | _ -> bad_vernac_args "EndSection")
 
 (* Proof switching *)
@@ -602,7 +618,7 @@ let _ =
        | [VARG_IDENTIFIER id] -> 
 	   (fun () -> 
 	      if_verbose show_script ();
-              save_anonymous false (string_of_id id))
+              save_anonymous false id)
        | _ -> bad_vernac_args "DefinedAnonymous")
 
 let _ =
@@ -612,11 +628,11 @@ let _ =
 	   (fun () -> 
 	      let (strength, opacity) = interp_definition_kind kind in
 	      if_verbose show_script ();
-              save_anonymous_with_strength strength opacity (string_of_id id))
+              save_anonymous_with_strength strength opacity id)
        | [VARG_IDENTIFIER id] -> 
 	   (fun () -> 
 	      if_verbose show_script ();
-              save_anonymous true (string_of_id id))
+              save_anonymous true id)
        | _ -> bad_vernac_args "SaveAnonymous")
 
 let _ =
@@ -859,7 +875,7 @@ let _ =
 let _ =
   add "TheoremProof"
     (function 
-       | [VARG_STRING kind; VARG_IDENTIFIER s; 
+       | [VARG_STRING kind; VARG_IDENTIFIER id;
 	  VARG_CONSTR com; VARG_VARGLIST coml] ->
 	   let calls = List.map
 			 (function 
@@ -872,7 +888,7 @@ let _ =
               try
             	States.with_heavy_rollback
 		  (fun () ->
-                     start_proof_com (Some s) stre com;
+                     start_proof_com (Some id) stre com;
                      if_verbose show_open_subgoals ();
                      List.iter Vernacinterp.call calls;
                      if_verbose show_script ();
@@ -884,19 +900,19 @@ let _ =
                                 const_entry_type = _},_)) = cook_proof () in
                        let cutt = vernac_tactic ("Cut",[Constr csr])
                        and exat = vernac_tactic ("Exact",[Constr pft]) in
-                       delete_proof s;
-                       by (tclTHENS cutt [introduction s;exat]))
+                       delete_proof id;
+                       by (tclTHENS cutt [introduction id;exat]))
 		  ()
               with e ->
             	if (is_unsafe "proof") && not (kind = "LETTOP") then begin
-                  mSGNL [< 'sTR "Warning: checking of theorem "; pr_id s;
+                  mSGNL [< 'sTR "Warning: checking of theorem "; pr_id id;
                            'sPC; 'sTR "failed";
                            'sTR "... converting to Axiom" >];
-                  delete_proof s;
-                  let _ = parameter_def_var (string_of_id s) com in ()
+                  delete_proof id;
+                  let _ = parameter_def_var id com in ()
            	end else 
 		  errorlabstrm "Vernacentries.TheoremProof"
-                    [< 'sTR "checking of theorem "; pr_id s; 'sPC;
+                    [< 'sTR "checking of theorem "; pr_id id; 'sPC;
                        'sTR "failed... aborting" >])
        | _ -> bad_vernac_args "TheoremProof")
 
@@ -961,12 +977,9 @@ let _ =
 	     List.iter 
 	       (fun (sl,c) -> 
 		  List.iter 
-		    (fun s ->
-                       let ref = 
-			 hypothesis_def_var 
-			   (refining()) (string_of_id s) stre c in
-                       if coe then
-			 Class.try_add_new_coercion ref stre)
+		    (fun id ->
+                       let ref = hypothesis_def_var (refining()) id stre c in
+                       if coe then Class.try_add_new_coercion ref stre)
                     sl)
 	       slcl
        | _ -> bad_vernac_args "VARIABLE")
@@ -982,7 +995,7 @@ let _ =
 	       (fun (sl,c) ->
 		  List.iter 
 		    (fun s -> 
-		       let _ = parameter_def_var (string_of_id s) c in ())
+		       let _ = parameter_def_var s c in ())
 		    sl)
                slcl
        | _ -> bad_vernac_args "PARAMETER")
@@ -1018,7 +1031,7 @@ let _ =
 
 let extract_qualid = function 
   | VARG_QUALID qid ->
-      (try wd_of_sp (fst (Nametab.locate_module qid))
+      (try Nametab.locate_loaded_library qid
        with Not_found -> 
 	 error ("Module/section "^(Nametab.string_of_qualid qid)^" not found"))
   | _ -> bad_vernac_args "extract_qualid"
@@ -1196,7 +1209,7 @@ let _ =
 		  | _ -> bad_vernac_args "RECORD")
                cfs in
            let const = match namec with 
-             | [] -> (id_of_string ("Build_"^(string_of_id struc)))
+             | [] -> add_prefix "Build_" struc
              | [VARG_IDENTIFIER id] -> id 
              | _ -> bad_vernac_args "RECORD" in
            let iscoe = (coe = "COERCION") in
@@ -1276,27 +1289,10 @@ let _ =
 	      syntax_definition id (aux com n))
        | _ -> bad_vernac_args "SyntaxMacro")
 
-(***
-let _ =
-  add "ABSTRACTION"
-    (function 
-       | (VARG_IDENTIFIER id) :: (VARG_CONSTR com) :: l ->
-	   (fun () ->
-              let arity = 
-		Array.of_list
-		  (List.map (function | (VARG_NUMBER n) -> n
-                               | _ -> bad_vernac_args "") l)
-              in 
-	      abstraction_definition id arity com;
-              if_verbose
-                message ((string_of_id id)^" is now an abstraction"))
-       | _ -> bad_vernac_args "ABSTRACTION")
-***)
-
 let _ =
   add "Require"
     (function 
-       | [VARG_STRING import; VARG_STRING specif; VARG_IDENTIFIER id] ->
+       | [VARG_STRING import; VARG_STRING specif; VARG_QUALID qid] ->
 	   fun () -> 
 	     without_mes_ambig 
 	       (Library.require_module 
@@ -1304,7 +1300,7 @@ let _ =
 		     None 
 		   else 
 		     Some (specif="SPECIFICATION"))
-		  (string_of_id id) None)
+		  qid None)
       	       (import="EXPORT") 
        | _ -> bad_vernac_args "Require")
 
@@ -1312,7 +1308,7 @@ let _ =
   add "RequireFrom"
     (function 
        | [VARG_STRING import; VARG_STRING specif;
-      	  VARG_IDENTIFIER id; VARG_STRING filename] ->
+      	  VARG_QUALID qid; VARG_STRING filename] ->
 	   (fun () -> 
 	      without_mes_ambig 
 		(Library.require_module 
@@ -1320,7 +1316,7 @@ let _ =
 		      None 
 		    else 
 		      Some (specif="SPECIFICATION"))
-		   (string_of_id id) (Some filename))
+		   qid (Some filename))
 		(import="EXPORT"))
        | _ -> bad_vernac_args "RequireFrom")
 
@@ -1416,22 +1412,22 @@ let _ =
 let _ =
   add "GRAMMAR"
     (function
-       | [VARG_IDENTIFIER univ; VARG_ASTLIST al] ->
-           (fun () -> Metasyntax.add_grammar_obj (string_of_id univ) al)
+       | [VARG_STRING univ; VARG_ASTLIST al] ->
+           (fun () -> Metasyntax.add_grammar_obj univ al)
        | _ -> bad_vernac_args "GRAMMAR")
 
 let _ =
   add "SYNTAX"
     (function
-       | [VARG_IDENTIFIER whatfor; VARG_ASTLIST sel] ->
-           (fun () -> Metasyntax.add_syntax_obj (string_of_id whatfor) sel)
+       | [VARG_STRING whatfor; VARG_ASTLIST sel] ->
+           (fun () -> Metasyntax.add_syntax_obj whatfor sel)
        | _ -> bad_vernac_args "SYNTAX")
     
 let _ =
   add "TACDEF"
     (let rec tacdef_fun lacc=function
         (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl ->
-          tacdef_fun ((string_of_id name,tacexp)::lacc) tl
+          tacdef_fun ((name,tacexp)::lacc) tl
        |[] ->
          fun () ->
            List.iter (fun (name,ve) -> Tacinterp.add_tacdef name ve) lacc
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index a0b434b9a4..f1d38494f4 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -82,10 +82,8 @@ let rec cvt_varg ast =
 	VARG_VARGLIST (List.map cvt_varg l)
     | Node(_,"VERNACCALL",(Str (_,na))::l) ->
         VCALL (na,List.map cvt_varg l)
-    | Node(_,"VERNACCALL",(Id (_,na))::l) ->
-        VCALL (na,List.map cvt_varg l)
 
-    | Nvar(_,s) -> VARG_IDENTIFIER (id_of_string s)
+    | Nvar(_,id) -> VARG_IDENTIFIER id
     | Node(loc,"QUALIDARG",p) -> VARG_QUALID (Astterm.interp_qualid p)
     | Node(loc,"QUALIDCONSTARG",p) ->
 	let q = Astterm.interp_qualid p in
@@ -94,13 +92,14 @@ let rec cvt_varg ast =
 	  with Not_found -> Nametab.error_global_not_found_loc loc q
 	in VARG_CONSTANT sp
     | Str(_,s) -> VARG_STRING s
+    | Id(_,s) -> VARG_STRING s
     | Num(_,n) -> VARG_NUMBER n
     | Node(_,"NONE",[]) -> VARG_UNIT
     | Node(_,"CONSTR",[c]) -> VARG_CONSTR c
     | Node(_,"CONSTRLIST",l) -> VARG_CONSTRLIST l
     | Node(_,"TACTIC",[c]) -> VARG_TACTIC c
     | Node(_,"BINDER",c::idl) ->
-        VARG_BINDER(List.map (compose id_of_string nvar_of_ast) idl, c)
+        VARG_BINDER(List.map nvar_of_ast idl, c)
     | Node(_,"BINDERLIST",l) ->
         VARG_BINDERLIST
           (List.map (compose (function