diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/indschemes.ml | 9 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 13 |
2 files changed, 2 insertions, 20 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c2c27eb78e..44d6f37cc6 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 _ = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c76ced56fd..6714b98f50 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1287,7 +1287,7 @@ let _ = let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "automatic introduction of variables"; optkey = ["Automatic";"Introduction"]; optread = Flags.is_auto_intros; @@ -1383,17 +1383,6 @@ let _ = optread = (fun () -> !CClosure.share); optwrite = (fun b -> CClosure.share := b) } -(* No more undo limit in the new proof engine. - The command still exists for compatibility (e.g. with ProofGeneral) *) - -let _ = - declare_int_option - { optdepr = true; - optname = "the undo limit (OBSOLETE)"; - optkey = ["Undo"]; - optread = (fun _ -> None); - optwrite = (fun _ -> ()) } - let _ = declare_bool_option { optdepr = false; |