Mini-nettoyage noms longs

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

4 files changed, 18 insertions, 29 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index a7a2552ff..e785644a5 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -163,9 +163,6 @@ let pr_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s])
 (*s Directory paths = section names paths *)
 type dir_path = string list
 
-(* The root of absolute names *)
-let coq_root = []
-
 (*s Section paths are absolute names *)
 
 type section_path = {
@@ -181,15 +178,15 @@ let basename sp = sp.basename
 let dirpath sp = sp.dirpath
 
 let qualid_of_sp sp =
-  make_qualid (coq_root @ dirpath sp) (string_of_id (basename sp))
+  make_qualid (dirpath sp) (string_of_id (basename sp))
 
 (* parsing and printing of section paths *)
-let string_of_dirpath sl = String.concat "." (coq_root@sl)
+let string_of_dirpath sl = String.concat "." sl
 
 let string_of_path sp =
   let (sl,id,k) = repr_path sp in
   String.concat ""
-    (List.flatten (List.map (fun s -> [s;"."]) (coq_root@sl))
+    (List.flatten (List.map (fun s -> [s;"."]) sl)
      @ [ string_of_id id ])
 
 let parse_sp s =
diff --git a/kernel/names.mli b/kernel/names.mli
index a96534f51..cca174463 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -51,8 +51,6 @@ val kind_of_string : string -> path_kind
 (*s Directory paths = section names paths *)
 type dir_path = string list
 
-val coq_root : dir_path
-
 (* Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b50d3af4b..5f7b4fbea 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -48,11 +48,15 @@ let add_include s alias =
   Mltop.dir_ml_dir s;
   Library.add_path s alias
 
+let add_coq_include s = add_include s [Nametab.coq_root]
+
 let add_rec_include s alias = 
   let subdirs = all_subdirs s (Some alias) in
   List.iter (fun lpe -> Mltop.dir_ml_dir lpe.directory) subdirs;
   List.iter Library.add_load_path_entry subdirs
 
+let add_coq_rec_include s = add_rec_include s [Nametab.coq_root]
+
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
 let push_include (s, alias) = includes := (s,alias,false) :: !includes
@@ -70,19 +74,19 @@ let init_load_path () =
   if Coq_config.local then begin
     (* local use (no installation) *)
     List.iter 
-      (fun s -> add_include (Filename.concat Coq_config.coqtop s) ["Coq"])
+      (fun s -> add_coq_include (Filename.concat Coq_config.coqtop s))
       ["states"; "dev"];
-    add_rec_include (Filename.concat Coq_config.coqtop "theories") ["Coq"];
-    add_include (Filename.concat Coq_config.coqtop "tactics") ["Coq"];
-    add_rec_include (Filename.concat Coq_config.coqtop "contrib") ["Coq"];
+    add_coq_rec_include (Filename.concat Coq_config.coqtop "theories");
+    add_coq_include (Filename.concat Coq_config.coqtop "tactics");
+    add_coq_rec_include (Filename.concat Coq_config.coqtop "contrib");
   end else begin
     (* default load path; variable COQLIB overrides the default library *)
     let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
-    add_rec_include coqlib ["Coq"]
+    add_coq_rec_include coqlib
   end;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
   add_ml_include camlp4;
-  add_include "." ["Scratch"];
+  add_include "." [Nametab.default_root];
   (* additional loadpath, given with -I -include -R options *)
   List.iter 
     (fun (s,alias,reci) ->
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 402e732c1..ebd291e37 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -29,21 +29,11 @@ let outputstate = ref ""
 let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
-let coqpath d =
-  let alias = Filename.basename d in
-  let alias =
-    if alias = "." then
-      Filename.basename (Unix.getcwd ())
-    else if alias = ".." then
-      Filename.basename (Filename.dirname (Unix.getcwd ()))
-    else alias in
-  if not (Names.is_ident alias) then 
-    error ("Cannot find a name to which "^d^" may map in Coq library");
-  alias
 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 load_vernacular_list = ref ([] : string list)
 let add_load_vernacular s =
   load_vernacular_list := (make_suffix s ".v") :: !load_vernacular_list
@@ -99,11 +89,11 @@ let parse_args () =
     | [] -> ()
 
     | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
-    | ("-I"|"-include") :: d :: rem -> set_include d (coqpath d); parse rem
+    | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
     | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p; parse rem
-    | "-R" :: d :: rem -> set_rec_include d (coqpath d); parse rem
+    | "-R" :: d :: rem -> set_default_rec_include d; parse rem
     | "-R" :: []       -> usage ()
 
     | "-q" :: rem -> no_load_rc (); parse rem