From a6757b089e1d268517bcba48a9fe33aa47526de2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 00:06:32 +0100
Subject: Remove Refine Instance Mode option

---
 test-suite/success/Typeclasses.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 3888cafed3..736d05fefc 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -198,9 +198,7 @@ Module UniqueInstances.
       for it. *)
   Set Typeclasses Unique Instances.
   Class Eq (A : Type) : Set.
-    Set Refine Instance Mode.
-    Instance eqa : Eq nat := _. constructor. Qed.
-    Unset Refine Instance Mode.
+    Instance eqa : Eq nat. Qed.
     Instance eqb : Eq nat := {}.
     Class Foo (A : Type) (e : Eq A) : Set.
     Instance fooa : Foo _ eqa := {}.
-- 
cgit v1.2.3