X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=ab5c1897bbbfc5785204bbf54d8a7ec35d98f742;hb=07fb52e761b192a97c6fe00c657e670b2d1fc2f1;hp=7586d41ac6c611ea31dd9f0c0ee0fc59437ec347;hpb=4ae7d510a430a2a6929f973d36b993d528772d64;p=helm.git

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