From 412b5ba92f3c76c6bdb7dada0ef7be62f72518a8 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 26 Nov 2019 11:30:20 +0100
Subject: Remove deprecated Typeclasses Axioms Are Instances.

---
 test-suite/success/Typeclasses.v | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'test-suite/success/Typeclasses.v')

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