blob: 66668930c7c0fde160b08dd3e433c37c46d4dffa (
plain)
1
2
3
|
Fail Notation "( x , y , .. , z )" := ltac:(let r := constr:(prod .. (prod x y) .. z) in r).
(* The command has indeed failed with message:
=> Error: Special token .. is for use in the Notation command. *)
|