diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-13 16:07:46 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-13 16:08:46 +0200 |
| commit | 505a6a2cb01eea3b4f60b9e9b3b583b56f1bd50b (patch) | |
| tree | a863d2e62e1c4db81c88ed48e4bad71a4a9f20d5 /toplevel | |
| parent | f8f65b0227056d49dc31174c89ea0da4427e3b56 (diff) | |
Deprecate options -dont, -lazy, -force-load-proofs.
These options no longer have any impact on the way proofs are loaded. In
other words, loading is always lazy, whatever the options. Keeping them
just so that coqc dies when the user prints some opaque symbol does not
seem worth it.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
| -rw-r--r-- | toplevel/usage.ml | 4 |
2 files changed, 3 insertions, 7 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d772171e5..edb03fb62 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -373,10 +373,8 @@ let parse_args arglist = |"-color" -> Flags.make_term_color true |"-config"|"--config" -> print_config := true |"-debug" -> set_debug () - |"-dont-load-proofs" -> Flags.load_proofs := Flags.Dont |"-emacs" -> set_emacs () |"-filteropts" -> filter_opts := true - |"-force-load-proofs" -> Flags.load_proofs := Flags.Force |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () |"--help-XML-protocol" -> Serialize.document Xml_printer.to_string_fmt; exit 0 @@ -384,7 +382,6 @@ let parse_args arglist = |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet |"-indices-matter" -> Indtypes.enforce_indices_matter () |"-just-parsing" -> Vernac.just_parsing := true - |"-lazy-load-proofs" -> Flags.load_proofs := Flags.Lazy |"-m"|"--memory" -> memory_stat := true |"-noinit"|"-nois" -> load_init := false |"-no-compat-notations" -> no_compat_ntn := true @@ -413,6 +410,9 @@ let parse_args arglist = warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs () |"-v7" -> error "This version of Coq does not support v7 syntax" |"-v8" -> warning "Obsolete option \"-v8\"." + |"-lazy-load-proofs" -> warning "Obsolete option \"-lazy-load-proofs\"." + |"-dont-load-proofs" -> warning "Obsolete option \"-dont-load-proofs\"." + |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"." (* Unknown option *) | s -> extras := s :: !extras diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 9851cfe87..e8e0292bc 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -67,10 +67,6 @@ let print_usage_channel co command = \n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\ \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ - -\n -force-load-proofs load opaque proofs in memory initially\ -\n -lazy-load-proofs load opaque proofs in memory by necessity (default)\ -\n -dont-load-proofs see opaque proofs as axioms instead of loading them\ \n -xml export XML files either to the hierarchy rooted in\ \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ |