From bed0e8790b9ee6cfc5410505f5c31fe52be8f77e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 4 Mar 2018 10:55:48 +0100 Subject: [compat] Remove NOOP and alias deprecated options. Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP. --- vernac/indschemes.ml | 7 ------- 1 file changed, 7 deletions(-) (limited to 'vernac/indschemes.ml') diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 447c5085b..8da87fd8e 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -59,13 +59,6 @@ let _ = optkey = ["Nonrecursive";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; optwrite = (fun b -> bifinite_elim_flag := b) } -let _ = - declare_bool_option - { optdepr = true; (* compatibility 2014-09-03*) - optname = "automatic declaration of induction schemes for non-recursive types"; - optkey = ["Record";"Elimination";"Schemes"]; - optread = (fun () -> !bifinite_elim_flag) ; - optwrite = (fun b -> bifinite_elim_flag := b) } let case_flag = ref false let _ = -- cgit v1.2.3