X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicSubstitution.mli;h=68311c68c0f6d4919be1848bab8de11e49ce17be;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=36291fb184b284971cf8e81c36cb1aaf09fc124d;hpb=4e3d7b4b47f66f0745333bfd4efcb27b4528f4c3;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.mli b/helm/software/components/cic_proof_checking/cicSubstitution.mli
index 36291fb18..68311c68c 100644
--- a/helm/software/components/cic_proof_checking/cicSubstitution.mli
+++ b/helm/software/components/cic_proof_checking/cicSubstitution.mli
@@ -35,11 +35,16 @@ exception ReferenceToInductiveDefinition;;
 (* since it needs to restrict the metavariables in case of failure      *)
 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
 
+(* lift map t *)
+(* as lift_from but lifts indexes by applying a map to them
+   the first argument of the map is the current depth *)
+(* FG: this is used in CicDischarge to perform non-linear relocation *)
+val lift_map: int -> (int -> int -> int) -> Cic.term -> Cic.term
+
 (* subst t1 t2                                                         *)
 (* substitutes [t1] for [Rel 1] in [t2]                                *)
 (* if avoid_beta_redexes is true (default: false) no new beta redexes  *)