From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 tools/coqdep.ml | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

(limited to 'tools/coqdep.ml')

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 79662a5d..a7c32e1d 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -9,6 +9,7 @@
 open Printf
 open Coqdep_lexer
 open Coqdep_common
+open System
 
 (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot])
     are now in [Coqdep_common]. The code that remains here concerns
@@ -459,21 +460,14 @@ let rec parse = function
   | "-boot" :: ll -> option_boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
   | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll
-  | "-I" :: r :: "-as" :: ln :: ll ->
-     add_rec_dir_no_import add_known r [];
-     add_rec_dir_no_import add_known r (split_period ln);
-     parse ll
-  | "-I" :: r :: "-as" :: [] -> usage ()
   | "-I" :: r :: ll -> add_caml_dir r; parse ll
   | "-I" :: [] -> usage ()
-  | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll
-  | "-R" :: r :: "-as" :: [] -> usage ()
   | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll
   | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll
   | "-R" :: ([] | [_]) -> usage ()
   | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll
   | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
-  | "-exclude-dir" :: r :: ll -> norec_dirnames := StrSet.add r !norec_dirnames; parse ll
+  | "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse ll
   | "-exclude-dir" :: [] -> usage ()
   | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
   | "-coqlib" :: [] -> usage ()
@@ -497,17 +491,18 @@ let coqdep () =
   if !option_boot then begin
     add_rec_dir_import add_known "theories" ["Coq"];
     add_rec_dir_import add_known "plugins" ["Coq"];
+    add_caml_dir "tactics";
     add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
     add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
   end else begin
-    Envars.set_coqlib ~fail:Errors.error;
+    Envars.set_coqlib ~fail:CErrors.error;
     let coqlib = Envars.coqlib () in
     add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
     if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
-      (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x)));
+      (Envars.xdg_dirs (fun x -> Feedback.msg_warning (Pp.str x)));
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
   end;
   List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
@@ -530,6 +525,6 @@ let coqdep () =
 let _ =
   try
     coqdep ()
-  with Errors.UserError(s,p) ->
+  with CErrors.UserError(s,p) ->
     let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
-    Pp.msgerrnl pp
+    Feedback.msg_error pp
-- 
cgit v1.2.3