matitaprover

[helm.git] / components / tactics / paramodulation / subst.mli

diff --git a/components/tactics/paramodulation/subst.mli b/components/tactics/paramodulation/subst.mli
index 9c124d9633502900162b760365add3ee62a02f2f..6627bf067c055037bc85d1b39fd19a3c9b6d947f 100644 (file)
--- a/components/tactics/paramodulation/subst.mli
+++ b/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 :