Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de

chemin physique : expansion uniquement pour Load, Add LoadPath, Declare ML
Module, Cd, ... mais pas pour les options -I, -boot, -R, -load-vernac-file, ...


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

3 files changed, 16 insertions, 10 deletions

diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 4449137e8..591b7b5a8 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -42,9 +42,8 @@ open Vernacinterp
 
 (* This path is where we look for .cmo *)
 let coq_mlpath_copy = ref ["."]
-let keep_copy_mlpath s = 
-  let dir = glob s in
-  coq_mlpath_copy := dir :: !coq_mlpath_copy
+let keep_copy_mlpath path = 
+  coq_mlpath_copy := path :: !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
 type toplevel = { 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 746a9a9f4..185bfd93c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -119,6 +119,7 @@ let pr_new_syntax loc ocom =
 let rec vernac_com interpfun (loc,com) =
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
+	let fname = expand_path_macros fname in
         (* translator state *)
         let ch = !chan_translate in
         let cs = Lexer.com_state() in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5ae3998f3..db30d7b95 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -597,28 +597,34 @@ let vernac_proof_instr instr =
 (* Auxiliary file management *)
 
 let vernac_require_from export spec filename =
-  Library.require_library_from_file None filename export
+  Library.require_library_from_file None
+    (System.expand_path_macros filename)
+    export
 
 let vernac_add_loadpath isrec pdir ldiropt =
+  let pdir = System.expand_path_macros pdir in
   let alias = match ldiropt with
     | None -> Nameops.default_root_prefix
     | Some ldir -> ldir in
   (if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias
 
-let vernac_remove_loadpath = Library.remove_load_path
+let vernac_remove_loadpath path =
+  Library.remove_load_path (System.expand_path_macros path)
 
   (* Coq syntax for ML or system commands *)
 
-let vernac_add_ml_path isrec s =
-  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (System.glob s)
+let vernac_add_ml_path isrec path =
+  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir)
+    (System.expand_path_macros path)
 
-let vernac_declare_ml_module l = Mltop.declare_ml_modules l
+let vernac_declare_ml_module l =
+  Mltop.declare_ml_modules (List.map System.expand_path_macros l)
 
 let vernac_chdir = function
   | None -> message (Sys.getcwd())
-  | Some s ->
+  | Some path ->
       begin
-	try Sys.chdir (System.glob s)
+	try Sys.chdir (System.expand_path_macros path)
 	with Sys_error str -> warning ("Cd failed: " ^ str)
       end;
       if_verbose message (Sys.getcwd())