tagging rc-1

[helm.git] / components / acic_procedural / acic2Procedural.ml

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index cc4ec10a340e9793999d5b09bbd3d12b4dcd40c8..b4f6053c04e493f2dcd5271ee74ebf0f3589e0c9 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -201,6 +201,7 @@ let mk_convert st ?name sty ety note =
    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) -> 
@@ -294,7 +295,8 @@ and proc_letin st what name v t =
                  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          ->