aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/EqNotation.v
blob: 21076472b811d5eabbd6f720c93fdc7232e8ebf8 (plain)
1
2
(* should mention "the implicit parameter A of eq" *)
Fail Type (forall x, x = x).