Very experimental commit: the type of the source is now required in LetIns

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

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index b4f6053c04e493f2dcd5271ee74ebf0f3589e0c9..18b4f064f71bfaccfadddb83acf4f62d57e3166b 100644 (file)
--- 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