X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsubst.mli;h=6627bf067c055037bc85d1b39fd19a3c9b6d947f;hb=eeed0d603ddadba6b5ee5041e87794051b9283dd;hp=3bbf7d00cb2f322b680d250f84f4e4fba6d18106;hpb=5b911ecf8bcb1644b82316d5f2709ae253a6a36d;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/subst.mli b/helm/software/components/tactics/paramodulation/subst.mli
index 3bbf7d00c..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 : 
@@ -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