(* This used to raise an anomaly *)

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