X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=a6e0667b05de904d64209c177889ea06b3f37daa;hb=186c1171d37f5d1cde9bb6f38a863be16debf3f0;hp=dd59d1f6e5305dfb74b04ea21dd7c035a21f62b1;hpb=54522577365be23b788d66c851ae5c78aebe5ffb;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index dd59d1f6e..a6e0667b0 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -202,8 +202,8 @@ let mk_convert st ?name sty ety note =
 	 [T.Note note]
       else []
    in
-   assert (Ut.is_sober csty); 
-   assert (Ut.is_sober cety);
+   assert (Ut.is_sober st.context csty); 
+   assert (Ut.is_sober st.context cety);
    if Ut.alpha_equivalence csty cety then script else 
    let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
    match name with
@@ -266,11 +266,14 @@ let mk_fwd_rewrite st dtext name tl direction v t ity =
 	 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
+	 else begin
+	    assert (Ut.is_sober st.context (H.cic ity));
+	    let ity = H.acic_bc st.context ity in
 	    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)]
+	 end
       | _                         -> assert false
 
 let mk_rewrite st dtext where qs tl direction t = 
@@ -305,8 +308,9 @@ and proc_letin st what name v w t =
 	       | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl  ->
 	          mk_fwd_rewrite st dtext intro tl false v t ity
 	       | v                                                     ->
+	          assert (Ut.is_sober st.context (H.cic ity));
+		  let ity = H.acic_bc st.context ity in
 	          let qs = [proc_proof (next st) v; [T.Id ""]] in
-	          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