Now iterating superposition

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

diff --git a/helm/software/components/ng_paramodulation/clauses.mli b/helm/software/components/ng_paramodulation/clauses.mli
index 81738c2a42314d221825a4a591bab474588c66f1..b857eb01629d5f0ceda19eb4d375a748d881b789 100644 (file)
--- a/helm/software/components/ng_paramodulation/clauses.mli
+++ b/helm/software/components/ng_paramodulation/clauses.mli
@@ -22,7 +22,9 @@ module Clauses (B : Orderings.Blob) :
 
     val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool
     val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int      
-    val fresh_clause : int -> B.t Terms.clause -> B.t Terms.clause * int
+    val fresh_clause : int ->
+         ?subst: B.t Terms.substitution ->
+         B.t Terms.clause -> B.t Terms.clause * int
 
     val mk_clause : int -> B.t Terms.foterm list -> B.t Terms.foterm list
                            -> B.t Terms.foterm -> B.t Terms.clause * int
@@ -40,4 +42,10 @@ module Clauses (B : Orderings.Blob) :
     val are_alpha_eq_cl :
            B.t Terms.clause -> B.t Terms.clause -> bool
 
+    val vars_of_clause :
+           B.t Terms.clause -> int list
+
+    (*val apply_subst :
+          B.t Terms.substitution -> B.t Terms.clause -> B.t Terms.clause*)
+
 end