From 84e9fc5da618e9e2248ba4a650b07b6b5528f957 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 23 Feb 2018 15:34:26 +0100
Subject: Remove deprecated options related to typeclasses.

---
 test-suite/bugs/closed/3513.v | 20 --------------------
 1 file changed, 20 deletions(-)

(limited to 'test-suite/bugs/closed')

diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index 5adc48215e..1f0f3b0da9 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -69,26 +69,6 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     refine (P _ _)
   end; unfold Basics.flip.
   Focus 2.
-  Set Typeclasses Debug.
-  Set Typeclasses Legacy Resolution.
-  apply reflexivity.
-  (* Debug: 1.1: apply @IsPointed_catOP on
-(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0))
-Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0))
-Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x))
-Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails)
-Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities
-Debug: Backtracking after apply @Equivalence_Reflexive
-Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails)
-Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails)
-Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred)
-*)
-  Undo. Unset Typeclasses Legacy Resolution.
-  Test Typeclasses Unique Solutions.
-  Test Typeclasses Unique Instances.
-  Show Existentials.
-  Set Typeclasses Debug Verbosity 2.
-  Set Printing All.
   (* As in 8.5, allow a shelved subgoal to remain *)
   apply reflexivity.
   
-- 
cgit v1.2.3