some more functors and a nice higher-order all_positions iterator

[helm.git] / helm / software / components / ng_paramodulation / foSubst.mli

diff --git a/helm/software/components/ng_paramodulation/foSubst.mli b/helm/software/components/ng_paramodulation/foSubst.mli
index dd7e0c2ec04075f56f7da90750a5a30fa628bdd0..74845d28aa090433342c49078859f00a6ae7539d 100644 (file)
--- a/helm/software/components/ng_paramodulation/foSubst.mli
+++ b/helm/software/components/ng_paramodulation/foSubst.mli
@@ -20,4 +20,9 @@ module Subst (B : Terms.Blob) :
     val lookup_subst : 
           int -> B.t Terms.substitution -> B.t Terms.foterm
     val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist
+    val apply_subst : 
+          B.t Terms.substitution -> B.t Terms.foterm -> B.t Terms.foterm
+    val concat: 
+          B.t Terms.substitution -> B.t Terms.substitution -> 
+            B.t Terms.substitution
   end