test-suite/bugs/closed/7712.v


1
2
3
4

(* This used to raise an anomaly *)

Fail Reserved Notation "'[tele_arg' x ';' .. ';' z ]"
       (format "[tele_arg '[hv'  x .. z ']' ]").