exported lift_from

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 38f2e7a6d484c617b8e838d523a3372843e599c6..aff9437575beab1ea7e65aacacf4175dc42ddf84 100644 (file)
--- 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 =

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index 3aff92f96c7cf0b2b6c79d1ec688049f3752394a..9083212ae6737ece3a855c865f9bda6c79037be0 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.mli
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
@@ -33,6 +33,10 @@ exception ReferenceToInductiveDefinition;;
 (* lifts [t] of [n] *)
 val lift : int -> Cic.term -> Cic.term
 
+(* lift from n t *)
+(* as lift but lifts only indexes >= from *)
+val lift_from: int -> int -> Cic.term -> Cic.term
+
 (* subst t1 t2                          *)
 (* substitutes [t1] for [Rel 1] in [t2] *)
 val subst : Cic.term -> Cic.term -> Cic.term