Procedural : tentative update to the new letin cic construction

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

diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml
index b3a247b02c448ca53aa7070a677d8f4574f97ef6..324141af46b0783c535ab07eab7720dbdb801663 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralConversion.ml
+++ b/helm/software/components/acic_procedural/proceduralConversion.ml
@@ -210,9 +210,9 @@ let get_clears c p xtypes =
            else 
               hd, names, v
         in
-        let p = C.LetIn (n, v, assert false, p) in
-        let it = C.LetIn (n, v, assert false, it) in
-        let et = C.LetIn (n, v, assert false, et) in
+        let p = C.LetIn (n, v, x, p) in
+        let it = C.LetIn (n, v, x, it) in
+        let et = C.LetIn (n, v, x, et) in
         aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Decl v) as hd :: tl     ->
         let p = C.Lambda (n, meta, p) in
@@ -220,9 +220,9 @@ let get_clears c p xtypes =
         let et = C.Lambda (n, meta, et) in
         aux (hd :: c) names p it et tl
       | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl ->
-        let p = C.LetIn (n, meta, assert false, p) in
-        let it = C.LetIn (n, meta, assert false, it) in
-        let et = C.LetIn (n, meta, assert false, et) in
+        let p = C.LetIn (n, meta, meta, p) in
+        let it = C.LetIn (n, meta, meta, it) in
+        let et = C.LetIn (n, meta, meta, et) in
         aux (hd :: c) names p it et tl
       | None :: tl                                        -> assert false
    in