X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fclauses.mli;h=b857eb01629d5f0ceda19eb4d375a748d881b789;hb=0842258ce37ce992a0d52c813a9a5cb4c3f2bb52;hp=81738c2a42314d221825a4a591bab474588c66f1;hpb=b714e87e96f14f332a5157567a4c62a4b28fa8eb;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/clauses.mli b/helm/software/components/ng_paramodulation/clauses.mli
index 81738c2a4..b857eb016 100644
--- 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