X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsubst.mli;h=6627bf067c055037bc85d1b39fd19a3c9b6d947f;hb=4ab3123d6a8e5080009d7b471b0cefd05f4817ed;hp=9c124d9633502900162b760365add3ee62a02f2f;hpb=2cd538bfba517fa5a300f3b5d32afaa380a7f59f;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/subst.mli b/helm/software/components/tactics/paramodulation/subst.mli
index 9c124d963..6627bf067 100644
--- a/helm/software/components/tactics/paramodulation/subst.mli
+++ b/helm/software/components/tactics/paramodulation/subst.mli
@@ -27,6 +27,7 @@ type substitution
 
 val empty_subst : substitution
 val apply_subst : substitution -> Cic.term -> Cic.term
+val apply_subst_lift : int -> substitution -> Cic.term -> Cic.term
 val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv
 val ppsubst : ?names:(Cic.name option list) -> substitution -> string
 val buildsubst :