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/success/old_typeclass.v | 13 ------------- 1 file changed, 13 deletions(-) delete mode 100644 test-suite/success/old_typeclass.v (limited to 'test-suite/success') diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v deleted file mode 100644 index 01e35810b..000000000 --- a/test-suite/success/old_typeclass.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Setoid Coq.Classes.Morphisms. -Set Typeclasses Legacy Resolution. - -Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and. - -Axiom In : Prop. -Axiom union_spec : In <-> True. - -Lemma foo : In /\ True. -Proof. -progress rewrite union_spec. -repeat constructor. -Qed. -- cgit v1.2.3