Merge remote-tracking branch 'origin/v8.5' into upstream-trunk

- Had to add a Sigma.to_evar_map
- Had to rework coqdep_common.ml{,i} and coqdep.ml

1 files changed, 29 insertions, 10 deletions

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 2cdb66aa7..221f3406b 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -210,6 +210,18 @@ let absolute_file_name basename odir =
   let dir = match odir with Some dir -> dir | None -> "." in
   absolute_dir dir // basename
 
+(** [find_dir_logpath dir] Return the logical path of directory [dir]
+    if it has been given one. Raise [Not_found] otherwise. In
+    particular we can check if "." has been attributed a logical path
+    after processing all options and silently give the default one if
+    it hasn't. We may also use this to warn if ap hysical path is met
+    twice.*)
+let register_dir_logpath,find_dir_logpath =
+  let tbl: (string, string list) Hashtbl.t = Hashtbl.create 19 in
+  let reg physdir logpath = Hashtbl.add tbl (absolute_dir physdir) logpath in
+  let fnd physdir = Hashtbl.find tbl (absolute_dir physdir) in
+  reg,fnd
+
 let file_name s = function
   | None     -> s
   | Some "." -> s
@@ -329,7 +341,8 @@ let escape =
     Buffer.contents s'
 
 let compare_file f1 f2 =
-  absolute_dir (Filename.dirname f1) = absolute_dir (Filename.dirname f2)
+  absolute_file_name (Filename.basename f1) (Some (Filename.dirname f1))
+  = absolute_file_name (Filename.basename f2) (Some (Filename.dirname f2))
 
 let canonize f =
   let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
@@ -509,11 +522,12 @@ let add_known recur phys_dir log_dir f =
 let is_not_seen_directory phys_f =
   not (StrSet.mem phys_f !norec_dirs)
 
-let rec add_directory add_file phys_dir log_dir =
+let rec add_directory recur add_file phys_dir log_dir =
+  register_dir_logpath phys_dir log_dir;
   let f = function
     | FileDir (phys_f,f) ->
-        if is_not_seen_directory phys_f then
-          add_directory add_file phys_f (log_dir @ [f])
+        if is_not_seen_directory phys_f && recur then
+          add_directory true add_file phys_f (log_dir @ [f])
     | FileRegular f ->
         add_file phys_dir log_dir f
   in
@@ -523,24 +537,29 @@ let rec add_directory add_file phys_dir log_dir =
   else
     warning_cannot_open_dir phys_dir
 
+(** Simply add this directory and imports it, no subdirs. This is used
+    by the implicit adding of the current path (which is not recursive). *)
+let add_norec_dir_import add_file phys_dir log_dir =
+  try add_directory false (add_file true) phys_dir log_dir with Unix_error _ -> ()
+
 (** -Q semantic: go in subdirs but only full logical paths are known. *)
-let add_dir add_file phys_dir log_dir =
-  try add_directory (add_file false) phys_dir log_dir with Unix_error _ -> ()
+let add_rec_dir_no_import add_file phys_dir log_dir =
+  try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> ()
 
 (** -R semantic: go in subdirs and suffixes of logical paths are known. *)
-let add_rec_dir add_file phys_dir log_dir =
-  add_directory (add_file true) phys_dir log_dir
+let add_rec_dir_import add_file phys_dir log_dir =
+  add_directory true (add_file true) phys_dir log_dir
 
 (** -R semantic but only on immediate capitalized subdirs *)
 
 let add_rec_uppercase_subdirs add_file phys_dir log_dir =
   process_subdirectories (fun phys_dir f ->
-    add_directory (add_file true) phys_dir (log_dir@[String.capitalize f]))
+    add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f]))
     phys_dir
 
 (** -I semantic: do not go in subdirs. *)
 let add_caml_dir phys_dir =
-  add_directory add_caml_known phys_dir []
+  add_directory false add_caml_known phys_dir []
 
 let rec treat_file old_dirname old_name =
   let name = Filename.basename old_name