Commit 90b9e0a6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Perform intros before abstraction, since abstraction would otherwise erase the...

Perform intros before abstraction, since abstraction would otherwise erase the goal due to the presence of quantifiers.
The bug was introduced in 589890aa.
parent 2923f216
...@@ -332,10 +332,10 @@ let print_task env pr thpr ?old:_ fmt task = ...@@ -332,10 +332,10 @@ let print_task env pr thpr ?old:_ fmt task =
| Tapp(ls,_) -> not (Sid.mem ls.ls_name info.info_symbols) | Tapp(ls,_) -> not (Sid.mem ls.ls_name info.info_symbols)
| _ -> true) true f) | _ -> true) true f)
])) task in ])) task in
let task = Trans.apply (Trans.lookup_transform "introduce_premises" env) task in
let task = Trans.apply (Abstraction.abstraction let task = Trans.apply (Abstraction.abstraction
(fun ls -> Sid.mem ls.ls_name info.info_symbols) (fun ls -> Sid.mem ls.ls_name info.info_symbols)
) task in ) task in
let task = Trans.apply (Trans.lookup_transform "introduce_premises" env) task in
(* (*
eprintf "Abstraction: @\n%a@." Pretty.print_task task; eprintf "Abstraction: @\n%a@." Pretty.print_task 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