Quelle  bug_13078.v   Sprache: Coq

(* 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).