match where with
| C.ARel (_, _, i, premise) as v ->
let where = Some (premise, name) in
- let _script = convert_elim st ~name:(premise, i) t v e in
+(* let _script = convert_elim st ~name:(premise, i) t v e in *)
let script = mk_arg st what @ mk_arg st v (* @ script *) in
let st = {st with context = Cn.clear st.context premise} in
st, T.Rewrite (direction, what, where, e, dtext) :: script
assert (List.length tl = 5);
let predicate = List.nth tl 2 in
let e = Cn.mk_pattern 1 predicate in
- let script = convert_elim st t t e in
+ let script = [] (* convert_elim st t t e *) in
script @ [T.Rewrite (direction, where, None, e, dtext); T.Branch (qs, "")]
let rec proc_lambda st name v t =
let predicate = List.nth tl (parsno - i) in
let e = Cn.mk_pattern j predicate in
let using = Some hd in
- convert_elim st what what e @ script @
+ (* convert_elim st what what e @ *) script @
[T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
| None ->
let qs = proc_bkd_proofs (next st) synth [] classes tl in