diff options
| author | Théo Zimmermann | 2018-02-23 15:34:26 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-03-04 19:40:22 +0100 |
| commit | 84e9fc5da618e9e2248ba4a650b07b6b5528f957 (patch) | |
| tree | fef97f79ef48048c98e6ca2c5238d544e3294dc7 /test-suite/bugs/closed | |
| parent | 78551857a41a57607ecfb3fd010e0a9755f47cea (diff) | |
Remove deprecated options related to typeclasses.
Diffstat (limited to 'test-suite/bugs/closed')
| -rw-r--r-- | test-suite/bugs/closed/3513.v | 20 |
1 files changed, 0 insertions, 20 deletions
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. |