From d331543b7b759bb97ea1ece32501cd0149627e9f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Apr 2017 16:37:11 +0200
Subject: Adding a test for the correctness of normalization in legacy
 typeclasses.

This is a test for commit 9d1230d484a2cf519f9cd76dc0f37815f3c6339b.
---
 test-suite/success/old_typeclass.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/success/old_typeclass.v

diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v
new file mode 100644
index 0000000000..01e35810b0
--- /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.
-- 
cgit v1.2.3