X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=7c66cc40bced62d6e3a889a38164627513a41064;hb=95a14ced97592a4116485f94c6ffa806feb62dbc;hp=a6d1a87432f71acc0c47cdfa44492b78e092ec64;hpb=948bb5d710c5d7f3185b6fef76c8e71f247cc664;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index a6d1a8743..7c66cc40b 100644
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -25,8 +25,7 @@ module type Blob =
 
     (* these could be outside the module, but to ease experimentation
      * we allow them to be tied with the ordering *)
-    val compute_unit_clause_weight : 't Terms.unit_clause -> int
-    val compute_goal_weight : 't Terms.unit_clause -> int
+    val compute_clause_weight : 't Terms.clause -> int
 
     val name : string