Ported demodulation on clauses

[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 885e97607077dcca3b682a9a34316a57692453d4..81738c2a42314d221825a4a591bab474588c66f1 100644 (file)
--- a/helm/software/components/ng_paramodulation/clauses.mli
+++ b/helm/software/components/ng_paramodulation/clauses.mli
@@ -37,4 +37,7 @@ module Clauses (B : Orderings.Blob) :
     val compare_passive_clauses_age :
            int * B.t Terms.clause -> int * B.t Terms.clause -> int
 
+    val are_alpha_eq_cl :
+           B.t Terms.clause -> B.t Terms.clause -> bool
+
 end