parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic_unification / cicReplace.ml

diff --git a/helm/software/components/cic_unification/cicReplace.ml b/helm/software/components/cic_unification/cicReplace.ml
index 7f53e1ee50422d0dc377ca58a27328a4dad4342f..0b8b674976d25d2c26aed41fb62b6210a8fb7cd1 100644 (file)
--- 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