From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 5 Jan 2005 14:07:33 +0000 (+0000)
Subject: exported lift_from
X-Git-Tag: V_0_1_0~153
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=21d58727027699d8617a7faab912843756b585ed;p=helm.git

exported lift_from
---

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 =
diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.mli b/helm/ocaml/cic_proof_checking/cicSubstitution.mli
index 3aff92f96..9083212ae 100644
--- 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