X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicSubstitution.ml;h=d111b15b58d52c70d2f7a733a2ea92ca2468fb62;hb=32d3f10c1904d450ce8ea3525230acc6980a5601;hp=ba2c8f723146308b65967e5f69ac9c0f13cbe183;hpb=d344d41028275b6d1451dca8e40a88e33e588389;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml
index ba2c8f723..d111b15b5 100644
--- a/helm/software/components/cic_proof_checking/cicSubstitution.ml
+++ b/helm/software/components/cic_proof_checking/cicSubstitution.ml
@@ -40,7 +40,7 @@ let debug_print =
   fun _  -> ()
 ;;
 
-let lift_from k n =
+let lift_map k map =
  let rec liftaux k =
   let module C = Cic in
    function
@@ -48,7 +48,7 @@ let lift_from k n =
        if m < k then
         C.Rel m
        else
-        C.Rel (m + n)
+        C.Rel (map k m)
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' = 
         List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
@@ -108,6 +108,9 @@ let lift_from k n =
  in
  liftaux k
 
+let lift_from k n =
+   lift_map k (fun _ m -> m + n)
+
 let lift n t =
   if n = 0 then
    t