blob: 12a4e8fc1aa7c3d97755384540679bf997853fcd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(*Congruence is weaker than reflexivity when it comes to higher level than necessary equalities:*)
Goal @eq Set nat nat.
congruence.
Qed.
Goal @eq Type nat nat.
congruence. (*bug*)
Qed.
Variable T : Type.
Goal @eq Type T T.
congruence.
Qed.
|