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.
---
 lib/flags.ml  | 4 ----
 lib/flags.mli | 3 ---
 2 files changed, 7 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 9ef32989c8..cd9d9d6900 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
diff --git a/lib/flags.mli b/lib/flags.mli
index 2ce78d8827..3bcea384eb 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
-- 
cgit v1.2.3