Commit e3d472a1 authored by Andrei Paskevich's avatar Andrei Paskevich

flatten context in

parent bfd52e95
......@@ -86,7 +86,9 @@ let extract_goals ctxt =
Transform.apply Transform.extract_goals ctxt
let transform env l =
let l = (fun t -> t,t.th_ctxt) (Typing.list_theory l) in
let l =
(fun t -> t, Context.use_export Context.empty_context t)
(Typing.list_theory l) in
let l = Transform.apply transformation l in
if !print_stdout then
List.iter (fun (t,ctxt) -> Why3.print_context_th std_formatter t.th_name ctxt) l
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment