test-suite/bugs/closed/4718.v


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.