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.

7 files changed, 4 insertions, 36 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 67cb50c29..172af9730 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 9ef32989c..cd9d9d690 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 2ce78d882..3bcea384e 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 a9cdf1f2f..fc74d25b4 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 c48873c80..2f64a24ab 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 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)\