blob: 14232e85786eaecffe6f2cf21de9a0d4087f8028 (
plain)
1
2
3
4
5
6
7
|
(* Was causing a stack overflow before #11613 *)
Declare Custom Entry bla.
Notation "[ t ]" := (t) (at level 0, t custom bla at level 0).
Notation "] t [" := (t) (in custom bla at level 0, t custom bla at level 0).
Notation "t" := (t) (in custom bla at level 0, t constr at level 9).
Notation "0" := (0) (in custom bla at level 0).
Check fun x => [ ] x [ ].
|
