From 505a6a2cb01eea3b4f60b9e9b3b583b56f1bd50b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 13 Jun 2014 16:07:46 +0200
Subject: 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.
---
 library/library.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index a9cdf1f2f8..fc74d25b45 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
-- 
cgit v1.2.3