blob: 1321a8598c290ac950290a98be198cf3e89ac6e9 (
plain)
1
2
3
4
5
6
7
8
|
Notation bar := ltac:(exact I).
Notation foo := bar (only parsing).
Class baz := { x : False }.
Instance: baz.
Admitted.
Definition baz0 := ((_ : baz) = (_ : baz)).
Definition foo1 := (foo = foo).
Definition baz1 := prod ((_ : baz) = (_ : baz)) (foo = foo).
|
