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.
---
 test-suite/bugs/closed/3481.v         | 4 ++--
 test-suite/bugs/closed/3520.v         | 2 +-
 test-suite/bugs/closed/3662.v         | 2 +-
 test-suite/bugs/closed/HoTT_coq_077.v | 2 +-
 test-suite/bugs/closed/HoTT_coq_104.v | 2 +-
 test-suite/success/letproj.v          | 2 +-
 test-suite/success/primitiveproj.v    | 2 +-
 7 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'test-suite')

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 }.
-- 
cgit v1.2.3