X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;fp=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=aff9437575beab1ea7e65aacacf4175dc42ddf84;hb=21d58727027699d8617a7faab912843756b585ed;hp=38f2e7a6d484c617b8e838d523a3372843e599c6;hpb=1850832c5f252cb6f79bce5184ccb9046a4057fb;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 38f2e7a6d..aff943757 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -30,7 +30,7 @@ exception ReferenceToConstant;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
-let lift n =
+let lift_from k n =
  let rec liftaux k =
   let module C = Cic in
    function
@@ -95,10 +95,13 @@ let lift n =
        in
         C.CoFix (i, liftedfl)
  in
+ liftaux k
+
+let lift n t =
   if n = 0 then
-   (function t -> t)
+   t
   else
-   liftaux 1
+   lift_from 1 n t
 ;;
 
 let subst arg =