Merge PR #6277: Qualified import in coqchk

2 files changed, 16 insertions, 20 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 44105aa72..82341ad9b 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -129,8 +129,6 @@ type logical_path = DirPath.t
 
 let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)
 
-let get_load_paths () = fst !load_paths
-
 (* Hints to partially detects if two paths refer to the same repertory *)
 let rec remove_path_dot p =
   let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
@@ -227,13 +225,8 @@ let locate_absolute_library dir =
 
 let locate_qualified_library qid =
   try
-    let loadpath =
-      (* Search library in loadpath *)
-      if qid.dirpath=[] then get_load_paths ()
-      else
-        (* we assume qid is an absolute dirpath *)
-        load_paths_of_dir_path (dir_of_path qid)
-    in
+    (* we assume qid is an absolute dirpath *)
+    let loadpath = load_paths_of_dir_path (dir_of_path qid) in
     if loadpath = [] then raise LibUnmappedDir;
     let name =  qid.basename^".vo" in
     let path, file = System.where_in_path loadpath name in
diff --git a/checker/checker.ml b/checker/checker.ml
index b2433ee36..fee31b667 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -96,17 +96,13 @@ let add_rec_path ~unix_path ~coq_root =
 
 (* By the option -include -I or -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) = includes := (s,alias) :: !includes
 
 let set_default_include d =
   push_include (d, Check.default_root_prefix)
 let set_include d p =
   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)
 
 (* Initializes the LoadPath *)
 let init_load_path () =
@@ -132,8 +128,7 @@ let init_load_path () =
   add_path ~unix_path:"." ~coq_root:Check.default_root_prefix;
   (* additional loadpath, given with -I -include -R options *)
   List.iter
-    (fun (unix_path, coq_root, reci) ->
-      if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root)
+    (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root)
     (List.rev !includes);
   includes := []
 
@@ -179,7 +174,9 @@ let print_usage_channel co command =
   output_string co command;
   output_string co "coqchk options are:\n";
   output_string co
-"  -R dir coqdir          map physical dir to logical coqdir\
+"  -Q dir coqdir          map physical dir to logical coqdir\
+\n  -R dir coqdir          synonymous for -Q\
+\n\
 \n\
 \n  -admit module          load module and dependencies without checking\
 \n  -norec module          check module but admit dependencies without checking\
@@ -311,6 +308,9 @@ let explain_exn = function
 	       report ())
   | e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
 
+let deprecated flag =
+  Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag))
+
 let parse_args argv =
   let rec parse = function
     | [] -> ()
@@ -324,12 +324,15 @@ let parse_args argv =
       Flags.coqlib_spec := true;
       parse rem
 
-    | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
+    | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem
     | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
-    | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
+    | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
+    | "-Q" :: d :: p :: rem -> set_include d p;parse rem
+    | "-Q" :: ([] | [_]) -> usage ()
+
+    | "-R" :: d :: p :: rem -> set_include d p;parse rem
     | "-R" :: ([] | [_]) -> usage ()
 
     | "-debug" :: rem -> set_debug (); parse rem