Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 3264cee2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove extraneous boxing in Coq printer.

parent 01fc55d2
...@@ -262,7 +262,7 @@ and print_tnode opl opr info fmt t = match t.t_node with ...@@ -262,7 +262,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
Number.print number_format fmt c Number.print number_format fmt c
| Tlet (t1,tb) -> | Tlet (t1,tb) ->
let v,t2 = t_open_bound tb in let v,t2 = t_open_bound tb in
fprintf fmt (protect_on opr "@[<hov>let %a :=@[<hov 1>@ %a@] in@ %a@]") fprintf fmt (protect_on opr "@[<hov>let %a :=@ %a in@ %a@]")
print_vs v (print_term info) t1 (print_opl_term info) t2; print_vs v (print_term info) t1 (print_opl_term info) t2;
forget_var v forget_var v
| Tcase (t,bl) -> | Tcase (t,bl) ->
...@@ -289,7 +289,7 @@ and print_tnode opl opr info fmt t = match t.t_node with ...@@ -289,7 +289,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
| Tapp (fs,pl) when is_fs_tuple fs -> | Tapp (fs,pl) when is_fs_tuple fs ->
fprintf fmt "%a" (print_paren_r (print_term info)) pl fprintf fmt "%a" (print_paren_r (print_term info)) pl
| Tapp (fs,[l;r]) when ls_equal fs fs_func_app -> | Tapp (fs,[l;r]) when ls_equal fs fs_func_app ->
fprintf fmt "(%a@ %a)" (print_opr_term info) l (print_opr_term info) r fprintf fmt "@[<hov 1>(%a@ %a)@]" (print_opr_term info) l (print_opr_term info) r
| Tapp (fs, tl) -> | Tapp (fs, tl) ->
begin match query_syntax info.info_syn fs.ls_name with begin match query_syntax info.info_syn fs.ls_name with
| Some s -> | Some s ->
...@@ -306,7 +306,7 @@ and print_tnode opl opr info fmt t = match t.t_node with ...@@ -306,7 +306,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
end end
| Tquant (Tforall,fq) -> | Tquant (Tforall,fq) ->
let vl,_tl,f = t_open_quant fq in let vl,_tl,f = t_open_quant fq in
fprintf fmt (protect_on opr "@[<hov>forall @[<hov>%a@],@ @[<hov>%a@]@]") fprintf fmt (protect_on opr "@[<hov>forall @[<hov>%a@],@ %a@]")
(print_list space (print_vsty info)) vl (print_list space (print_vsty info)) vl
(* (print_tl info) tl *) (print_term info) f; (* (print_tl info) tl *) (print_term info) f;
List.iter forget_var vl List.iter forget_var vl
...@@ -316,7 +316,7 @@ and print_tnode opl opr info fmt t = match t.t_node with ...@@ -316,7 +316,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
match vl with match vl with
| [] -> print_term info fmt f | [] -> print_term info fmt f
| v::vr -> | v::vr ->
fprintf fmt (protect_on opr "@[<hov>exists @[<hov>%a@],@ @[<hov>%a@]@]") fprintf fmt (protect_on opr "@[<hov>exists %a,@ %a@]")
(print_vsty_nopar info) v (print_vsty_nopar info) v
aux vr aux vr
in in
...@@ -338,7 +338,7 @@ and print_tnode opl opr info fmt t = match t.t_node with ...@@ -338,7 +338,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
fprintf fmt (protect_on opr "@[<hov>~ %a@]") (print_opl_term info) f fprintf fmt (protect_on opr "@[<hov>~ %a@]") (print_opl_term info) f
| Tif (f1,f2,f3) -> | Tif (f1,f2,f3) ->
fprintf fmt (protect_on opr fprintf fmt (protect_on opr
"@[<hov>if @[<hov>%a@] then@ @[<hov>%a@]@ else@ @[<hov>%a@]@]") "@[<hov>if %a then@ %a@ else@ %a@]")
(print_term info) f1 (print_term info) f2 (print_opl_term info) f3 (print_term info) f1 (print_term info) f2 (print_opl_term info) f3
and print_tbranch info fmt br = and print_tbranch info fmt br =
......
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