Vernacentries: minor code cleanup

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

1 files changed, 12 insertions, 15 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e100025dd..278e87418 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -807,37 +807,34 @@ let vernac_set_used_variables l =
 (*****************************)
 (* Auxiliary file management *)
 
+let expand filename =
+  Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename
+
 let vernac_require_from export filename =
-  Library.require_library_from_file None
-    (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) filename)
-    export
+  Library.require_library_from_file None (expand filename) export
 
 let vernac_add_loadpath isrec pdir ldiropt =
-  let pdir = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) 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) ~unix_path:pdir ~coq_root:alias
+  let pdir = expand pdir in
+  let alias = Option.default Nameops.default_root_prefix ldiropt in
+  (if isrec then Mltop.add_rec_path else Mltop.add_path)
+    ~unix_path:pdir ~coq_root:alias
 
 let vernac_remove_loadpath path =
-  Library.remove_load_path (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path)
+  Library.remove_load_path (expand path)
 
   (* Coq syntax for ML or system commands *)
 
 let vernac_add_ml_path isrec path =
-  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir)
-    (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path)
+  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (expand path)
 
 let vernac_declare_ml_module local l =
-  Mltop.declare_ml_modules local (List.map
-				    (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)))
-				    l)
+  Mltop.declare_ml_modules local (List.map expand l)
 
 let vernac_chdir = function
   | None -> msg_notice (str (Sys.getcwd()))
   | Some path ->
       begin
-	try Sys.chdir (Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) path)
+	try Sys.chdir (expand path)
 	with Sys_error err -> msg_warning (str ("Cd failed: " ^ err))
       end;
       if_verbose msg_info (str (Sys.getcwd()))