X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=7586d41ac6c611ea31dd9f0c0ee0fc59437ec347;hb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;hp=ccd6bf2864b4650174313446b6e1809b6b76f517;hpb=637114791874df9ebc4e0f0936513c71886a913f;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index ccd6bf286..7586d41ac 100644
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -22,4 +22,7 @@ module Orderings (B : Terms.Blob) :
     val compare_terms : 
           B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
 
+    val compute_unit_clause_weight :
+      B.t Terms.unit_clause -> int
+
   end