X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=18b4f064f71bfaccfadddb83acf4f62d57e3166b;hb=cc23f034c9419186602d9250456241f2eba90d7c;hp=b4f6053c04e493f2dcd5271ee74ebf0f3589e0c9;hpb=94538d45a28cf8e833f9ad4523b61a3252fde7d4;p=helm.git

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index b4f6053c0..18b4f064f 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -300,7 +300,8 @@ and proc_letin st what name v t =
 	    in
 	    st, C.Decl (H.cic ity), rqv
 	 | None          ->
-	    st, C.Def (H.cic v, None), [T.LetIn (intro, v, dtext)]
+            (*CSC: here we need the type of v *)
+	    st, C.Def (H.cic v, assert false), [T.LetIn (intro, v, dtext)]
       in
       let entry = Some (name, hyp) in
       let qt = proc_proof (next (add st entry intro)) t in
@@ -385,7 +386,7 @@ and proc_proof st t =
    in
    match t with
       | C.ALambda (_, name, w, t)        -> proc_lambda st name w t
-      | C.ALetIn (_, name, v, t) as what -> proc_letin (f st) what name v t
+      | C.ALetIn (_, name, v, ty, t) as what -> assert false (*proc_letin (f st) what name v t*)
       | C.ARel _ as what                 -> proc_rel (f st) what
       | C.AMutConstruct _ as what        -> proc_mutconstruct (f st) what
       | C.AAppl (_, hd :: tl) as what    -> proc_appl (f st) what hd tl