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

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

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index fb95a6d0c4cf4e842831398e5f7186ac99ae77ac..31c7f4e8d5058a4e16e8cc40b3b16c4800f3de9a 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -180,11 +180,11 @@ let cic_bc c t =
    let get_fix_decl (sname, i, w, v) = sname, w in
    let get_cofix_decl (sname, w, v) = sname, w in
    let rec bc c = function
-      | C.LetIn (name, v, t) ->
+      | C.LetIn (name, v, ty, t) ->
          let name = mk_fresh_name c name in
-         let entry = Some (name, C.Def (v, None)) in
-         let v, t = bc c v, bc (entry :: c) t in
-        C.LetIn (name, v, t)
+         let entry = Some (name, C.Def (v, ty)) in
+         let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+        C.LetIn (name, v, ty, t)
       | C.Lambda (name, w, t) ->
          let name = mk_fresh_name c name in
          let entry = Some (name, C.Decl w) in
@@ -222,11 +222,11 @@ let acic_bc c t =
    let get_fix_decl (id, sname, i, w, v) = sname, cic w in
    let get_cofix_decl (id, sname, w, v) = sname, cic w in
    let rec bc c = function
-      | C.ALetIn (id, name, v, t) ->
+      | C.ALetIn (id, name, v, ty, t) ->
          let name = mk_fresh_name c name in
-         let entry = Some (name, C.Def (cic v, None)) in
-         let v, t = bc c v, bc (entry :: c) t in
-        C.ALetIn (id, name, v, t)
+         let entry = Some (name, C.Def (cic v, cic ty)) in
+         let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+        C.ALetIn (id, name, v, ty, t)
       | C.ALambda (id, name, w, t) ->
          let name = mk_fresh_name c name in
          let entry = Some (name, C.Decl (cic w)) in