Commit b776e361 authored by Ralf Jung's avatar Ralf Jung

fix print spacing of telescopes

parent 48758ab8
......@@ -125,7 +125,7 @@ Proof. unfold tele_fun_compose. rewrite tele_app_bind. done. Qed.
(** Notation *)
Notation "'[tele' x .. z ]" :=
(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))
(x binder, z binder, format "[tele '[hv' x .. z ']' ]").
(x binder, z binder, format "[tele '[hv' x .. z ']' ]").
Notation "'[tele' ]" := (TeleO)
(format "[tele ]").
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment