6 files changed, 20 insertions, 35 deletions
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index fd6101bf89..c86548440b 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.12") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq811.
+Import Coq.Compat.Coq812.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index f774cef44f..a1c1209db6 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq812.
 Import Coq.Compat.Coq811.
 Import Coq.Compat.Coq810.
-Import Coq.Compat.Coq89.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..dd259988ac
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq812.
+Import Coq.Compat.Coq811.
+Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq89.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index 1c5ccc1a92..00f4747e3e 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq812.
 Import Coq.Compat.Coq811.
-Import Coq.Compat.Coq810.
diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v
index 22fb09526d..d944036112 100644
--- a/test-suite/success/LocalDefinition.v
+++ b/test-suite/success/LocalDefinition.v
@@ -26,28 +26,12 @@ Module TestAdmittedVisibility.
   Fail Check d2.
 End TestAdmittedVisibility.
 
-(* Test consistent behavior of Local Definition wrt automatic declaration of instances *)
-
 Module TestVariableAsInstances.
-  Module Test1.
-    Set Typeclasses Axioms Are Instances.
-    Class U.
-    Local Parameter b : U.
-    Definition testU := _ : U. (* _ resolved *)
-
-    Class T.
-    Variable a : T.  (* warned to be the same as "Local Parameter" *)
-    Definition testT := _ : T. (* _ resolved *)
-  End Test1.
-
-  Module Test2.
-    Unset Typeclasses Axioms Are Instances.
-    Class U.
-    Local Parameter b : U.
-    Fail Definition testU := _ : U. (* _ unresolved *)
+  Class U.
+  Local Parameter b : U.
+  Fail Definition testU := _ : U. (* _ unresolved *)
 
-    Class T.
-    Variable a : T.  (* warned to be the same as "Local Parameter" thus should not be an instance *)
-    Fail Definition testT := _ : T. (* used to succeed *)
-  End Test2.
+  Class T.
+  Variable a : T.  (* warned to be the same as "Local Parameter" thus should not be an instance *)
+  Fail Definition testT := _ : T. (* used to succeed *)
 End TestVariableAsInstances.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 736d05fefc..3f96bf2c35 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -241,13 +241,8 @@ Module IterativeDeepening.
 
 End IterativeDeepening.
 
-Module AxiomsAreInstances.
-  Set Typeclasses Axioms Are Instances.
-  Class TestClass1 := {}.
-  Axiom testax1 : TestClass1.
-  Definition testdef1 : TestClass1 := _.
+Module AxiomsAreNotInstances.
 
-  Unset Typeclasses Axioms Are Instances.
   Class TestClass2 := {}.
   Axiom testax2 : TestClass2.
   Fail Definition testdef2 : TestClass2 := _.
@@ -256,4 +251,4 @@ Module AxiomsAreInstances.
   Existing Instance testax2.
   Definition testdef2 : TestClass2 := _.
 
-End AxiomsAreInstances.
+End AxiomsAreNotInstances.