ng_disambiguation ng_kernel ng_refiner disambiguation: svn:ignore fixed

[helm.git] / helm / software / components / cic_proof_checking / cicSubstitution.ml

diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml
index ba2c8f723146308b65967e5f69ac9c0f13cbe183..d111b15b58d52c70d2f7a733a2ea92ca2468fb62 100644 (file)
--- 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