From 228a39aab291af446b9419673c05d224dfbd8a72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Nov 2014 16:51:27 +0100
Subject: Adding test for bug #3326.

---
 test-suite/bugs/closed/3326.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/3326.v

diff --git a/test-suite/bugs/closed/3326.v b/test-suite/bugs/closed/3326.v
new file mode 100644
index 0000000000..4d7e9f77cb
--- /dev/null
+++ b/test-suite/bugs/closed/3326.v
@@ -0,0 +1,19 @@
+Class ORDER A := Order {
+  LEQ : A -> A -> bool; 
+  leqRefl: forall x, true = LEQ x x
+}.
+
+Section XXX.
+
+Variable A:Type.
+Variable (O:ORDER A).
+Definition aLeqRefl := @leqRefl _ O.
+
+Lemma OK : forall x, true = LEQ x x.
+Proof.
+  intros.
+  unfold LEQ.
+  destruct O.
+  clear.
+  Fail apply aLeqRefl.
+Abort.
-- 
cgit v1.2.3