Merge PR #6896: [compat] Remove NOOP deprecated options.

10 files changed, 8 insertions, 29 deletions

diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 30724759d2..6004711235 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -127,7 +127,6 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}.
 \optindex{Boolean Equality Schemes}
 \optindex{Elimination Schemes}
 \optindex{Nonrecursive Elimination Schemes}
-\optindex{Record Elimination Schemes}
 \optindex{Case Analysis Schemes}
 \optindex{Decidable Equality Schemes}
 \optindex{Rewriting Schemes}
@@ -144,7 +143,6 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic
 declaration of the induction principles. It can be activated with the
 command {\tt Set Nonrecursive Elimination Schemes}. It can be
 deactivated again with {\tt Unset Nonrecursive Elimination Schemes}.
-{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}.
 
 In addition, the {\tt Case Analysis Schemes} flag governs the generation of
 case analysis lemmas for inductive types, i.e. corresponding to the
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 71cde0ca14..00c971237d 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -143,18 +143,6 @@ let newssrcongrtac arg ist gl =
 
 (** 7. Rewriting tactics (rewrite, unlock) *)
 
-(** Coq rewrite compatibility flag *)
-
-
-let _ =
-  let ssr_strict_match = ref false in
-  Goptions.declare_bool_option
-    { Goptions.optname  = "strict redex matching";
-      Goptions.optkey   = ["Match"; "Strict"];
-      Goptions.optread  = (fun () -> !ssr_strict_match);
-      Goptions.optdepr  = true; (* noop *)
-      Goptions.optwrite = (fun b -> ssr_strict_match := b) }
-
 (** Rewrite rules *)
 
 type ssrwkind = RWred of ssrsimpl | RWdef | RWeq
diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v
index 89d476dcb1..38f03b166b 100644
--- a/test-suite/bugs/closed/3481.v
+++ b/test-suite/bugs/closed/3481.v
@@ -3,7 +3,7 @@ Set Implicit Arguments.
 
 Require Import Logic.
 Module NonPrim.
-Local Set Record Elimination Schemes.
+Local Set Nonrecursive Elimination Schemes.
 Record prodwithlet (A B : Type) : Type :=
   pair' { fst : A; fst' := fst; snd : B }.
 
@@ -21,7 +21,7 @@ End NonPrim.
 
 Global Set Universe Polymorphism.
 Global Set Asymmetric Patterns.
-Local Set Record Elimination Schemes.
+Local Set Nonrecursive Elimination Schemes.
 Local Set Primitive Projections.
 
 Record prod (A B : Type) : Type :=
diff --git a/test-suite/bugs/closed/3520.v b/test-suite/bugs/closed/3520.v
index c981207e6b..ea122e521f 100644
--- a/test-suite/bugs/closed/3520.v
+++ b/test-suite/bugs/closed/3520.v
@@ -3,7 +3,7 @@ Set Primitive Projections.
 Record foo (A : Type) := 
   { bar : Type ; baz := Set; bad : baz = bar }.
 
-Set Record Elimination Schemes.
+Set Nonrecursive Elimination Schemes.
 
 Record notprim : Prop :=
   { irrel : True; relevant : nat }.
diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v
index bd53389b4f..b8754bce98 100644
--- a/test-suite/bugs/closed/3662.v
+++ b/test-suite/bugs/closed/3662.v
@@ -1,6 +1,6 @@
 Set Primitive Projections.
 Set Implicit Arguments.
-Set Record Elimination Schemes.
+Set Nonrecursive Elimination Schemes.
 Record prod A B := pair { fst : A ; snd : B }.
 Definition f : Set -> Type := fun x => x.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v
index 017780c1f3..f69c71a026 100644
--- a/test-suite/bugs/closed/HoTT_coq_077.v
+++ b/test-suite/bugs/closed/HoTT_coq_077.v
@@ -3,7 +3,7 @@ Set Implicit Arguments.
 Require Import Logic.
 
 Set Asymmetric Patterns.
-Set Record Elimination Schemes.
+Set Nonrecursive Elimination Schemes.
 Set Primitive Projections.
 
 Record prod (A B : Type) : Type :=
diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v
index 5bb7fa8c12..a6ff78d127 100644
--- a/test-suite/bugs/closed/HoTT_coq_104.v
+++ b/test-suite/bugs/closed/HoTT_coq_104.v
@@ -4,7 +4,7 @@ Require Import Logic.
 
 Global Set Universe Polymorphism.
 Global Set Asymmetric Patterns.
-Local Set Record Elimination Schemes.
+Local Set Nonrecursive Elimination Schemes.
 Local Set Primitive Projections.
 
 Record prod (A B : Type) : Type :=
diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v
index a183be6223..de2857b437 100644
--- a/test-suite/success/letproj.v
+++ b/test-suite/success/letproj.v
@@ -1,5 +1,5 @@
 Set Primitive Projections.
-Set Record Elimination Schemes.
+Set Nonrecursive Elimination Schemes.
 Record Foo (A : Type) := { bar : A -> A; baz : A }.
 
 Definition test (A : Type) (f : Foo A) := 
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 576bdbf71b..31a1608c4d 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -1,5 +1,5 @@
 Set Primitive Projections.
-Set Record Elimination Schemes.
+Set Nonrecursive Elimination Schemes.
 Module Prim.
 
 Record F := { a : nat; b : a = a }.
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 779926a7d7..41c44b126d 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -61,13 +61,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 _ =