X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fsubst.mli;h=6627bf067c055037bc85d1b39fd19a3c9b6d947f;hb=41e76668e9389ce17e41747026e533f907a0311c;hp=3bbf7d00cb2f322b680d250f84f4e4fba6d18106;hpb=9559b53134624dbee523cf6406a9852665c0ff77;p=helm.git

diff --git a/components/tactics/paramodulation/subst.mli b/components/tactics/paramodulation/subst.mli
index 3bbf7d00c..6627bf067 100644
--- 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 : 
@@ -39,5 +40,4 @@ val is_in_subst : int -> substitution -> bool
 val merge_subst_if_possible: 
   substitution -> substitution -> 
     substitution option
-val concat_substs: substitution -> substitution -> substitution
-
+val concat: substitution -> substitution -> substitution