[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.

10 files changed, 8 insertions, 29 deletions

diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index 30724759d..600471123 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 11ebe4337..449d132ce 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -141,18 +141,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 89d476dcb..38f03b166 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 c981207e6..ea122e521 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 bd53389b4..b8754bce9 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 017780c1f..f69c71a02 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 5bb7fa8c1..a6ff78d12 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 a183be622..de2857b43 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 576bdbf71..31a1608c4 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 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 _ =