X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=b4f6053c04e493f2dcd5271ee74ebf0f3589e0c9;hb=4f1bd2790a4448a8ebfbe67eb8baa481c124745c;hp=f39aa18bd96ee3a162baa10fa6da07ca3b6f8805;hpb=55ec3926f6fbb5dba13705659fe94d0db38b2666;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index f39aa18bd..b4f6053c0 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -198,7 +198,10 @@ let mk_convert st ?name sty ety note =
    let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
       note (Pp.ppterm csty) (Pp.ppterm cety)
    in
+   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) -> 
@@ -266,7 +269,7 @@ let mk_rewrite st dtext where qs tl direction t =
 let rec proc_lambda st name v t =
    let dno = DTI.does_not_occur 1 (H.cic t) in
    let dno = dno && match get_inner_types st t with
-      | None          -> true
+      | None          -> false
       | Some (it, et) -> 
          DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
    in
@@ -292,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          ->