Commit 45dffedf authored by Francois Bobot's avatar Francois Bobot

ajout de la transformation simplify_trivial_quantification_in_goal utilisation dans alt-ergo.drv

parent bc3b1ccc
......@@ -22,7 +22,7 @@ transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "simplify_trivial_quantification_in_goal"
theory BuiltIn
syntax type int "int"
......
......@@ -146,3 +146,21 @@ let simplify_trivial_quantification =
let () = Register.register_transform
"simplify_trivial_quantification" simplify_trivial_quantification
let on_goal fn =
let fn task = match task with
| Some {Task.task_decl =
Task.Decl ({d_node = Decl.Dprop (Pgoal,pr,fmla)});
task_prev = task_prev} ->
(List.fold_left Task.add_decl) task_prev (fn pr fmla)
| _ -> assert false in
Trans.store fn
let simplify_trivial_quantification_in_goal =
Register.store
(fun () -> on_goal (fun pr f ->
[create_prop_decl Pgoal pr (fmla_remove_quant f)]))
let () = Register.register_transform
"simplify_trivial_quantification_in_goal"
simplify_trivial_quantification_in_goal
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