diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 93476f4c4..e0f21aab8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -189,7 +189,8 @@ let parse_args arglist = | "-batch" :: rem -> set_batch_mode (); parse rem | "-boot" :: rem -> boot := true; no_load_rc (); parse rem | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem - | "-outputstate" :: s :: rem -> set_outputstate s; parse rem + | "-outputstate" :: s :: rem -> + Flags.load_proofs := Flags.Force; set_outputstate s; parse rem | "-outputstate" :: [] -> usage () | "-nois" :: rem -> set_inputstate ""; parse rem @@ -230,8 +231,9 @@ let parse_args arglist = | "-compile-verbose" :: f :: rem -> add_compile true f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem | "-compile-verbose" :: [] -> usage () - | "-load-proofs" :: rem -> Flags.load_proofs := true; parse rem - | "-dont-load-proofs" :: rem -> Flags.load_proofs := false; parse rem + | "-force-load-proofs" :: rem -> Flags.load_proofs := Flags.Force; parse rem + | "-lazy-load-proofs" :: rem -> Flags.load_proofs := Flags.Lazy; parse rem + | "-dont-load-proofs" :: rem -> Flags.load_proofs := Flags.Dont; parse rem | "-beautify" :: rem -> make_beautify true; parse rem |