diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-20 08:30:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-20 08:30:24 +0200 |
| commit | fb482f6b02156c1fcf029263083b0371e030a2cd (patch) | |
| tree | 99f3ee49f015b2859f627cf2e57db0eb5ef3cb27 /checker/checker.ml | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
[flags] Flag `open Flags`
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
Diffstat (limited to 'checker/checker.ml')
| -rw-r--r-- | checker/checker.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 7a69700d2..67b812133 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open System -open Flags open Names open Check @@ -74,7 +73,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d with CErrors.UserError _ -> - if_verbose Feedback.msg_warning + Flags.if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -342,7 +341,7 @@ let parse_args argv = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> boot := true; parse rem + | "-boot" :: rem -> Flags.boot := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem @@ -374,7 +373,7 @@ let init_with_argv argv = parse_args argv; if !Flags.debug then Printexc.record_backtrace true; Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); - if_verbose print_header (); + Flags.if_verbose print_header (); init_load_path (); engage (); with e -> |