Add an option -Q (tentative name).

This option complements -I-as and -R. As the two other options, it adds a
new loadpath, but contrarily to them, files are not looked into the
directory unless fully qualified.

7 files changed, 42 insertions, 31 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 005f6c4ec7..85a59c50ee 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,26 +59,26 @@ let load_rcfile() =
 
 (* Puts dir in the path of ML and in the LoadPath *)
 let coq_add_path unix_path s =
-  Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]);
+  Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true;
   Mltop.add_ml_dir unix_path
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
 let add_stdlib_path ~unix_path ~coq_root ~with_ml =
   if !Flags.load_init then
-    Mltop.add_rec_path ~unix_path ~coq_root
+    Mltop.add_rec_path ~unix_path ~coq_root ~implicit:true
   else
-    Mltop.add_path ~unix_path ~coq_root;
+    Mltop.add_path ~unix_path ~coq_root ~implicit:false;
   if with_ml then
     Mltop.add_rec_ml_dir unix_path
 
 let add_userlib_path ~unix_path =
-  Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix;
+  Mltop.add_path ~unix_path ~coq_root:Nameops.default_root_prefix ~implicit:false;
   Mltop.add_rec_ml_dir unix_path
 
 (* Options -I, -I-as, and -R of the command line *)
 let includes = ref []
-let push_include (s, alias) = includes := (s,alias,false) :: !includes
-let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
+let push_include s alias recursive implicit =
+  includes := (s,alias,recursive,implicit) :: !includes
 let ml_includes = ref []
 let push_ml_include s = ml_includes := s :: !ml_includes
 
@@ -104,11 +104,12 @@ let init_load_path () =
     (* then directories in COQPATH *)
     List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath;
     (* then current directory *)
-    Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix;
-    (* additional loadpath, given with options -I-as and -R *)
+    Mltop.add_path ~unix_path:"." ~coq_root:Nameops.default_root_prefix ~implicit:false;
+    (* additional loadpath, given with options -I-as, -Q, and -R *)
     List.iter
-      (fun (unix_path, coq_root, reci) ->
-	if reci then Mltop.add_rec_path ~unix_path ~coq_root else Mltop.add_path ~unix_path ~coq_root)
+      (fun (unix_path, coq_root, reci, implicit) ->
+        (if reci then Mltop.add_rec_path else Mltop.add_path)
+          ~unix_path ~coq_root ~implicit)
       (List.rev !includes);
     (* additional ml directories, given with option -I *)
     List.iter Mltop.add_ml_dir (List.rev !ml_includes)
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 4ca8b61f8c..942ef143b6 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -15,8 +15,9 @@ val set_rcfile : string -> unit
 val no_load_rc : unit -> unit
 val load_rcfile : unit -> unit
 
-val push_include : string * Names.DirPath.t -> unit
-val push_rec_include : string * Names.DirPath.t -> unit
+val push_include : string -> Names.DirPath.t -> bool -> bool -> unit
+(** [push_include phys_path log_path recursive implicit] *)
+
 val push_ml_include : string -> unit
 
 val init_load_path : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6d92eaa5a6..bf0c872cc3 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -73,13 +73,11 @@ let outputstate = ref ""
 let set_outputstate s = outputstate:=s
 let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
 
-let set_default_include d = push_include (d,Nameops.default_root_prefix)
-let set_include d p =
+let set_default_include d =
+  push_include d Nameops.default_root_prefix false false
+let set_include d p recursive implicit =
   let p = dirpath_of_string p in
-  push_include (d,p)
-let set_rec_include d p =
-  let p = dirpath_of_string p in
-  push_rec_include(d,p)
+  push_include d p recursive implicit
 
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
@@ -305,16 +303,21 @@ let parse_args arglist =
     (* Complex options with many args *)
     |"-I"|"-include" ->
       begin match rem with
-      | d :: "-as" :: p :: rem -> set_include d p; args := rem
+      | d :: "-as" :: p :: rem -> set_include d p false true; args := rem
       | d :: "-as" :: [] -> error_missing_arg "-as"
       | d :: rem -> push_ml_include d; args := rem
       | [] -> error_missing_arg opt
       end
+    |"-Q" ->
+      begin match rem with
+      | d :: p :: rem -> set_include d p true false; args := rem
+      | _ -> error_missing_arg opt
+      end
     |"-R" ->
       begin match rem with
-      | d :: "-as" :: p :: rem -> set_rec_include d p; args := rem
       | d :: "-as" :: [] -> error_missing_arg "-as"
-      | d :: p :: rem -> set_rec_include d p; args := rem
+      | d :: "-as" :: p :: rem
+      | d :: p :: rem -> set_include d p true true; args := rem
       | _ -> error_missing_arg opt
       end
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index e0cb2209d5..458fe8ef08 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -152,11 +152,13 @@ let add_rec_ml_dir unix_path =
 
 (* Adding files to Coq and ML loadpath *)
 
-let add_path ~unix_path:dir ~coq_root:coq_dirpath =
+let add_path ~unix_path:dir ~coq_root:coq_dirpath ~implicit =
   if exists_dir dir then
     begin
       add_ml_dir dir;
-      Loadpath.add_load_path dir true coq_dirpath
+      Loadpath.add_load_path dir
+        (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath)
+        coq_dirpath
     end
   else
     msg_warning (str ("Cannot open " ^ dir))
@@ -167,7 +169,7 @@ let convert_string d =
     msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
     raise Exit
 
-let add_rec_path ~unix_path ~coq_root =
+let add_rec_path ~unix_path ~coq_root ~implicit =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
     let prefix = Names.DirPath.repr coq_root in
@@ -180,9 +182,12 @@ let add_rec_path ~unix_path ~coq_root =
     let dirs = List.map_filter convert_dirs dirs in
     let () = List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs in
     let () = add_ml_dir unix_path in
-    let add (path, dir) = Loadpath.add_load_path path false dir in
-    let () = List.iter add dirs in
-    Loadpath.add_load_path unix_path true coq_root
+    let add (path, dir) =
+      Loadpath.add_load_path path Loadpath.ImplicitPath dir in
+    let () = if implicit then List.iter add dirs in
+    Loadpath.add_load_path unix_path
+      (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath)
+      coq_root
   else
     msg_warning (str ("Cannot open " ^ unix_path))
 
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 1b9257c617..19b9996317 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -43,8 +43,8 @@ val add_ml_dir : string -> unit
 val add_rec_ml_dir : string -> unit
 
 (** Adds a path to the Coq and ML paths *)
-val add_path : unix_path:string -> coq_root:Names.DirPath.t -> unit
-val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> unit
+val add_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
+val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool -> unit
 
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8343140948..73a5095778 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -20,9 +20,10 @@ let print_usage_channel co command =
   output_string co
 "  -I dir                 look for ML files in dir\
 \n  -include dir           (idem)\
-\n  -I dir -as coqdir      map physical dir to logical coqdir\
+\n  -I dir -as coqdir      implicitly map physical dir to logical coqdir\
 \n  -R dir -as coqdir      recursively map physical dir to logical coqdir\
 \n  -R dir coqdir          (idem)\
+\n  -Q dir coqdir          map physical dir to logical coqdir\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\
 \n  -notop                 set the toplevel name to be the empty logical path\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b948a05357..1854e11265 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -857,7 +857,7 @@ let vernac_add_loadpath isrec pdir ldiropt =
   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
+    ~unix_path:pdir ~coq_root:alias ~implicit:true
 
 let vernac_remove_loadpath path =
   Loadpath.remove_load_path (expand path)