assert (Ut.is_sober csty);
assert (Ut.is_sober cety);
if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else
+ let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
match name with
| None -> [T.Change (sty, ety, None, e, ""(*note*))]
| Some (id, i) ->
mk_fwd_rewrite st dtext intro tl false v
| v ->
let qs = [proc_proof (next st) v; [T.Id ""]] in
- st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
+ let ity = H.acic_bc st.context ity in
+ st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
in
st, C.Decl (H.cic ity), rqv
| None ->