Commit 56cfe3b2 authored by François Bobot's avatar François Bobot
Browse files

[Printer] why3 printer prelude should be placed after the theory opening

parent 2b67051b
......@@ -399,8 +399,9 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task =
(* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
(* forget_all (); *)
print_prelude fmt pr;
fprintf fmt "theory Task@\n";
print_th_prelude task fmt thpr;
fprintf fmt "theory Task@\n%a@\nend@."
fprintf fmt "%a@\nend@."
(print_list nothing string)
(List.rev (Trans.apply print_tdecls task))
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