summaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/3304.v
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. *)