blob: f73117a2ee148f211ded3c2e2ff2452174e2745e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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. *)
|
