1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3326.v b/test-suite/bugs/opened/3326.v
new file mode 100644
index 00000000..f73117a2
--- /dev/null
+++ b/test-suite/bugs/opened/3326.v
@@ -0,0 +1,18 @@
+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.
+  intros.
+  unfold LEQ.
+  destruct O.
+  clear.
+  Fail apply aLeqRefl. (* Toplevel input, characters 15-30:
+Anomaly: Uncaught exception Not_found(_). Please report. *)