aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2262.v
blob: b61f18b83737abb1fbbf0e31f596199ea33da141 (plain)
1
2
3
4
5
6
7
8
9
10
11


Generalizable Variables A.
Class Test A := { test : A }.

Lemma mylemma : forall `{Test A}, test = test.
Admitted. (* works fine *)

Definition mylemma' := forall `{Test A}, test = test.
About mylemma'.