Properly set module names in presence of -Q. (Fix for bug #3958)

This is done by adding a fourth type of loadpath, the ones that are
neither implicit nor root, for the subdirectories of a -Q root.

Note: this means that scanning for available directories is no longer done
on the fly for -Q, but once and for all, as with -R.

3 files changed, 20 insertions, 25 deletions

diff --git a/library/loadpath.ml b/library/loadpath.ml
index 5876eedd2..ab8b0a307 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -12,14 +12,13 @@ open Errors
 open Names
 open Libnames
 
-type path_type = ImplicitPath | ImplicitRootPath | RootPath
-
 (** Load paths. Mapping from physical to logical paths. *)
 
 type t = {
   path_physical : CUnix.physical_path;
   path_logical : DirPath.t;
-  path_type : path_type;
+  path_root : bool;
+  path_implicit : bool;
 }
 
 let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS"
@@ -54,13 +53,14 @@ let remove_load_path dir =
   let filter p = not (String.equal p.path_physical dir) in
   load_paths := List.filter filter !load_paths
 
-let add_load_path phys_path path_type coq_path =
+let add_load_path phys_path coq_path ~root ~implicit =
   let phys_path = CUnix.canonical_path_name phys_path in
   let filter p = String.equal p.path_physical phys_path in
   let binding = {
     path_logical = coq_path;
     path_physical = phys_path;
-    path_type = path_type;
+    path_root = root;
+    path_implicit = implicit;
   } in
   match List.filter filter !load_paths with
   | [] ->
@@ -93,7 +93,7 @@ let expand_root_path dir =
   let rec aux = function
   | [] -> []
   | p :: l ->
-    if p.path_type <> ImplicitPath && is_dirpath_prefix_of p.path_logical dir then
+    if p.path_root && is_dirpath_prefix_of p.path_logical dir then
       let suffix = drop_dirpath_prefix p.path_logical dir in
       extend_path_with_dirpath p.path_physical suffix :: aux l
     else aux l
@@ -123,13 +123,17 @@ let expand_path dir =
   let rec aux = function
   | [] -> []
   | p :: l ->
-    match p.path_type with
-    | ImplicitPath -> expand p dir :: aux l
-    | ImplicitRootPath ->
+    match p.path_implicit, p.path_root with
+    | true, false -> expand p dir :: aux l
+    | true, true ->
       let inters = intersections p.path_logical dir in
       List.map (expand p) inters @ aux l
-    | RootPath ->
+    | false, true ->
       if is_dirpath_prefix_of p.path_logical dir then
 	expand p (drop_dirpath_prefix p.path_logical dir) :: aux l
-      else aux l in
+      else aux l
+    | false, false ->
+      (* nothing to do, an explicit root path should also match above
+         if [is_dirpath_prefix_of p.path_logical dir] were true here *)
+      aux l in
   aux !load_paths
diff --git a/library/loadpath.mli b/library/loadpath.mli
index 62dc5d591..d4029303d 100644
--- a/library/loadpath.mli
+++ b/library/loadpath.mli
@@ -15,11 +15,6 @@ open Names
 
 *)
 
-type path_type =
-  | ImplicitPath     (** Can be implicitly appended to a logical path. *)
-  | ImplicitRootPath (** Can be implicitly appended to the suffix of a logical path. *)
-  | RootPath         (** Can only be a prefix of a logical path. *)
-
 type t
 (** Type of loadpath bindings. *)
 
@@ -35,7 +30,7 @@ val get_load_paths : unit -> t list
 val get_paths : unit -> CUnix.physical_path list
 (** Same as [get_load_paths] but only get the physical part. *)
 
-val add_load_path : CUnix.physical_path -> path_type -> DirPath.t -> unit
+val add_load_path : CUnix.physical_path -> DirPath.t -> root:bool -> implicit:bool -> unit
 (** [add_load_path phys type log] adds the binding [phys := log] to the current
     loadpaths. *)
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 9dc1dd5b1..357c5482f 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -165,9 +165,7 @@ 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
-        (if implicit then Loadpath.ImplicitRootPath else Loadpath.RootPath)
-        coq_dirpath
+      Loadpath.add_load_path dir ~root:true ~implicit coq_dirpath
     end
   else
     msg_warning (str ("Cannot open " ^ dir))
@@ -191,11 +189,9 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
     let dirs = List.map_filter convert_dirs dirs in
     let () = add_ml_dir unix_path in
     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
+      Loadpath.add_load_path path ~root:false ~implicit dir in
+    let () = List.iter add dirs in
+    Loadpath.add_load_path unix_path ~root:true ~implicit coq_root
   else
     msg_warning (str ("Cannot open " ^ unix_path))