7 files changed, 8 insertions, 8 deletions
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 }.