Commit 20349d93 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

gappa printer: inline all before

parent 72be2df9
......@@ -10,12 +10,12 @@ valid 0
unknown "no contradiction was found\\|some enclosures were not satisfied" "Unknown"
transformation "simplify_recursive_definition"
transformation "inline_trivial"
(* transformation "inline_trivial" *)
transformation "inline_all"
transformation "eliminate_builtin"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_if"
(* transformation "eliminate_if" *)
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
......
......@@ -355,8 +355,8 @@ let print_task env pr thpr ?old:_ fmt task =
let equations,hyps,goal =
List.fold_left (prepare info) ([],[],None) (Task.task_decls task)
in
List.iter (print_equation info fmt) equations;
fprintf fmt "@[<v 2>{ %a@\n%a }@\n@]" (print_list nothing (print_hyp info)) hyps
List.iter (print_equation info fmt) (List.rev equations);
fprintf fmt "@[<v 2>{ %a%a}@\n@]" (print_list nothing (print_hyp info)) hyps
(print_goal info) goal
(*
print_decls ?old info fmt (Task.task_decls 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