aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 9886b263c..a7c32e1d6 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -495,7 +495,7 @@ let coqdep () =
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"];
@@ -525,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
Feedback.msg_error pp