diff options
Diffstat (limited to 'test-suite/bugs/opened/3326.v')
-rw-r--r-- | test-suite/bugs/opened/3326.v | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/test-suite/bugs/opened/3326.v b/test-suite/bugs/opened/3326.v deleted file mode 100644 index f73117a2..00000000 --- a/test-suite/bugs/opened/3326.v +++ /dev/null @@ -1,18 +0,0 @@ -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. *) |