- | 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 = 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
+ | C.ARel (_, _, i, premise) as w ->
+(* let _script = convert_elim st ~name:(premise, i) v w e in *)
+ let script name =
+ let where = Some (premise, name) in
+ let script = mk_arg st what @ mk_arg st w (* @ script *) in
+ T.Rewrite (direction, what, where, e, dtext) :: script
+ in
+ if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then
+ {st with context = Cn.clear st.context premise}, script name
+ else
+ let br1 = [T.Id ""] in
+ let br2 = List.rev (T.Apply (w, "assumption") :: script None) in
+ let text = "non linear rewrite" in
+ st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)]