aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/indschemes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/indschemes.ml')
-rw-r--r--vernac/indschemes.ml9
1 files changed, 1 insertions, 8 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c2c27eb78..44d6f37cc 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -84,15 +84,8 @@ let _ =
optkey = ["Boolean";"Equality";"Schemes"];
optread = (fun () -> !eq_flag) ;
optwrite = (fun b -> eq_flag := b) }
-let _ = (* compatibility *)
- declare_bool_option
- { optdepr = true;
- optname = "automatic declaration of boolean equality";
- optkey = ["Equality";"Scheme"];
- optread = (fun () -> !eq_flag) ;
- optwrite = (fun b -> eq_flag := b) }
-let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
+let is_eq_flag () = !eq_flag
let eq_dec_flag = ref false
let _ =