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