Remove deprecated Typeclasses Axioms Are Instances.

2 files changed, 8 insertions, 29 deletions

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.