Mini-nettoyage noms longs

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

2 files changed, 15 insertions, 21 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b50d3af4b3..5f7b4fbeac 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 402e732c1f..ebd291e371 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