Adding test for bug #3326.

1 files changed, 19 insertions, 0 deletions

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.