added some code to print the praamodulation proofs with a graph

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

diff --git a/helm/software/components/tactics/paramodulation/subst.mli b/helm/software/components/tactics/paramodulation/subst.mli
index 3bbf7d00cb2f322b680d250f84f4e4fba6d18106..6627bf067c055037bc85d1b39fd19a3c9b6d947f 100644 (file)
--- 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