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