diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-06 16:57:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 01:10:55 +0200 |
| commit | 0b6f9dafdd828466ab87306f30f3aae0bc689f4f (patch) | |
| tree | a49004a54f6f5cd9af54ca630cc16016be4f6161 /tools | |
| parent | 2c52a8304ed2bab9fc110818160463f57ba8fccd (diff) | |
[coqdep] Remove unnecessary dependency on Pp and CError.
This allows for even earlier bootstrapping.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index d96cf57ce..7db0b2890 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -512,6 +512,9 @@ let rec parse = function | f :: ll -> treat_file None f; parse ll | [] -> () +(* Exception to be raised by Envars *) +exception CoqlibError of string + let coqdep () = if Array.length Sys.argv < 2 then usage (); if not Coq_config.has_natdynlink then option_dynlink := No; @@ -526,7 +529,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:(fun msg -> CErrors.user_err Pp.(str msg)); + Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg)); 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"]; @@ -557,6 +560,5 @@ let coqdep () = let _ = try coqdep () - with CErrors.UserError(s,p) -> - let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in - eprintf "%a@\n%!" Pp.pp_with pp + with CoqlibError msg -> + eprintf "*** Error: %s@\n%!" msg |