aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3326.v
blob: 4d7e9f77cbe80052a161b1cf6227cc19df4cdf79 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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.