aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/indschemes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/indschemes.ml')
-rw-r--r--vernac/indschemes.ml7
1 files changed, 0 insertions, 7 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index e90c25926..44d6f37cc 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -84,13 +84,6 @@ 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