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 /plugins/extraction | |
| 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 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/table.ml | 5 |
1 files changed, 1 insertions, 4 deletions
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 |