blob: ec04408fd100f4b9464e0f67b9ca7fb95791d053 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* Check that rules with patterns are not registered for cases patterns *)
Module PrintingTest.
Declare Custom Entry test.
Notation "& x" := (Some x) (in custom test at level 0, x pattern).
Check fun x => match x with | None => None | Some tt => Some tt end.
Notation "& x" := (Some x) (at level 0, x pattern).
Check fun x => match x with | None => None | Some tt => Some tt end.
End PrintingTest.
Fail Notation "x &" := (Some x) (at level 0, x pattern).
|
