aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/old_typeclass.v13
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v
new file mode 100644
index 000000000..01e35810b
--- /dev/null
+++ b/test-suite/success/old_typeclass.v
@@ -0,0 +1,13 @@
+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.