Commit 8af3190f authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Allow (again) applying transformation on proof attempt (apply on parent)

parent 7513458b
......@@ -387,11 +387,8 @@ let interp commands_table cont id s =
try
let t = Trans.lookup_trans cont.Controller_itp.controller_env cmd in
match id with
| Some (Session_itp.APn _id) -> Transform (cmd,t,args)
| Some (Session_itp.ATn _tid) -> Transform (cmd, t, args)
| Some (Session_itp.AFile _f) -> Transform (cmd, t, args)
| Some (Session_itp.ATh _th) -> Transform (cmd, t, args)
| _ -> QError ("Please select a goal or trans node in the task tree")
| Some _ -> Transform (cmd,t,args)
| None -> QError ("Please select a goal or trans node in the task tree")
with
| Trans.UnknownTrans _ ->
match parse_prover_name cont.Controller_itp.controller_config cmd args with
......
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