diff options
| -rw-r--r-- | doc/refman/RefMan-com.tex | 16 | ||||
| -rw-r--r-- | lib/flags.ml | 4 | ||||
| -rw-r--r-- | lib/flags.mli | 3 | ||||
| -rw-r--r-- | library/library.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 5 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
| -rw-r--r-- | toplevel/usage.ml | 4 |
7 files changed, 4 insertions, 36 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 67cb50c295..172af9730c 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -217,22 +217,6 @@ Section~\ref{LongNames}). This dumps references for global names in file {\em file} (to be used by coqdoc, see~\ref{coqdoc}) -\item[{\tt -dont-load-proofs}]\ - - In this mode, it is an error to access the body of opaque theorems - (for example via {\tt Print} or {\tt Print Assumptions}). - -\item[{\tt -lazy-load-proofs}]\ - - This is the default behavior. Proofs of opaque theorems aren't - loaded immediately in memory, but only when necessary, for instance - during a {\tt Print} or {\tt Print Assumptions}. This mode should be - almost as fast and efficient as {\tt -dont-load-proofs}. - -\item[{\tt -force-load-proofs}]\ - - Deprecated, now the same as {\tt -lazy-load-proofs}. - \item[{\tt -no-hash-consing}] \mbox{} \item[{\tt -vm}]\ diff --git a/lib/flags.ml b/lib/flags.ml index 9ef32989c8..cd9d9d6900 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -73,10 +73,6 @@ let ideslave_coqtop_flags = ref None let time = ref false -type load_proofs = Force | Lazy | Dont - -let load_proofs = ref Lazy - let raw_print = ref false let record_print = ref true diff --git a/lib/flags.mli b/lib/flags.mli index 2ce78d8827..3bcea384eb 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -39,9 +39,6 @@ val time : bool ref val we_are_parsing : bool ref -type load_proofs = Force | Lazy | Dont -val load_proofs : load_proofs ref - val raw_print : bool ref val record_print : bool ref val univ_print : bool ref diff --git a/library/library.ml b/library/library.ml index a9cdf1f2f8..fc74d25b45 100644 --- a/library/library.ml +++ b/library/library.ml @@ -347,8 +347,6 @@ let access_table fetch_table add_table tables dp i = assert (i < Array.length t); t.(i) let access_opaque_table dp i = - if !Flags.load_proofs == Flags.Dont then - error "Not accessing an opaque term due to option -dont-load-proofs."; access_table (fetch_table "opaque proofs") add_opaque_table !opaque_tables dp i diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index c48873c808..2f64a24ab3 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -299,10 +299,7 @@ let warning_axioms () = str "Having invalid logical axiom in the environment when extracting" ++ spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ fnl ()) - end; - if !Flags.load_proofs == Flags.Dont && not (List.is_empty (info_axioms@log_axioms)) then - msg_warning - (str "Some of these axioms might be due to option -dont-load-proofs.") + end let warning_opaques accessed = let opaques = Refset'.elements !opaques in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d772171e59..edb03fb62b 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 9851cfe87c..e8e0292bc9 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)\ |