X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Fprocedural2.ml;h=e41dd101b896b8f64bea8fbae0a22d6331d15c84;hb=5bb62857c7d6906da3ab6b52a23505b8e62e6d06;hp=dbd70428c7cba8195bc408b4fea6e46889fe3d5a;hpb=cdd3fc617825db73ce08a0cb700e2a8e115b4fb3;p=helm.git

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index dbd70428c..e41dd101b 100644
--- a/helm/software/components/acic_procedural/procedural2.ml
+++ b/helm/software/components/acic_procedural/procedural2.ml
@@ -204,7 +204,10 @@ let mk_convert st ?name sty ety note =
       | None         -> [T.Change (sty, ety, None, e, note)]
       | Some (id, i) -> 
          begin match get_entry st id with
-	    | C.Def _  -> assert false (* T.ClearBody (id, "") :: script *)
+	    | C.Def _  -> 
+	       [T.Change (ety, sty, Some (id, Some id), e, note);
+	        T.ClearBody (id, "")
+	       ]
 	    | C.Decl _ -> 
 	       [T.Change (ety, sty, Some (id, Some id), e, note)] 
          end
@@ -278,8 +281,10 @@ and proc_letin st what name v w t =
    let intro = get_intro name in
    let proceed, dtext = test_depth st in
    let script = if proceed then 
-      let st, hyp, rqv = match get_inner_types st v with
-         | Some (ity, _) ->
+      let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with
+         | Some (C.ALetIn _, _), _ ->
+	    st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)]
+	 | _, Some (ity, _)        ->
 	    let st, rqv = match v with
                | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl ->
 	          mk_fwd_rewrite st dtext intro tl true v t ity
@@ -292,7 +297,7 @@ and proc_letin st what name v w t =
 		  st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
 	    in
 	    st, C.Decl (H.cic ity), rqv
-	 | None          ->
+	 | _, None                 ->
 	    st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)]
       in
       let entry = Some (name, hyp) in