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 /lib/flags.ml | |
| 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 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 4 |
1 files changed, 0 insertions, 4 deletions
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 |