Skip to content

GitLab

why3
why3
Commit 3760cdb5 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

bitvectors/bitvector fullay proved thanks to CVC4 1.2

parent 122c0632
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 276 additions and 1292 deletions
src/whyml/mlw_ocaml.ml
View file @ 3760cdb5
......@@ -783,7 +783,7 @@ and print_lexpr pri info fmt e =
and print_rec lr info fst fmt { fun_ps = ps ; fun_lambda = lam } =
if ps.ps_ghost then
fprintf fmt "(* %s %a *)"
fprintf fmt "@[<hov 2>%s %a = ()@]"
(if fst then if lr then "let rec" else "let" else "with")
(print_ps info) ps
else
......
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