aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/options.ml3
-rw-r--r--lib/options.mli2
2 files changed, 0 insertions, 5 deletions
diff --git a/lib/options.ml b/lib/options.ml
index d5efe7feff..a8adcdb74e 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -64,6 +64,3 @@ let without_mes_ambig f x =
let unsafe_set = ref Stringset.empty
let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
let is_unsafe s = Stringset.mem s !unsafe_set
-
-(* To deal with two kinds of discharge *)
-let immediate_discharge = false
diff --git a/lib/options.mli b/lib/options.mli
index 84c60c9ddf..bf73cfcdf8 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -38,5 +38,3 @@ val without_mes_ambig : ('a -> 'b) -> 'a -> 'b
val add_unsafe : string -> unit
val is_unsafe : string -> bool
-
-val immediate_discharge : bool