X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicReplace.ml;h=0b8b674976d25d2c26aed41fb62b6210a8fb7cd1;hb=145583de619b9d2fcc4abe3f4d68d01538f9f394;hp=7f53e1ee50422d0dc377ca58a27328a4dad4342f;hpb=6ca04b596642894449012de8ec6d2f3f784f5868;p=helm.git

diff --git a/helm/software/components/cic_unification/cicReplace.ml b/helm/software/components/cic_unification/cicReplace.ml
index 7f53e1ee5..0b8b67497 100644
--- a/helm/software/components/cic_unification/cicReplace.ml
+++ b/helm/software/components/cic_unification/cicReplace.ml
@@ -42,7 +42,7 @@ let replace_lifting ~equality ~context ~what ~with_what ~where =
     find_image_aux (what,with_what)
   in
   let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
-  let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+  let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
   let rec substaux k ctx what t =
    try
     S.lift (k-1) (find_image ctx what t)
@@ -72,9 +72,9 @@ let replace_lifting ~equality ~context ~what ~with_what ~where =
     | C.Lambda (n,s,t) ->
        C.Lambda
         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
-    | C.LetIn (n,s,t) ->
+    | C.LetIn (n,s,ty,t) ->
        C.LetIn
-        (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
+        (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
        let tl' = List.map (substaux k ctx what) tl in