Various architectural changes

[helm.git] / helm / software / components / ng_paramodulation / orderings.mli

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index a6d1a87432f71acc0c47cdfa44492b78e092ec64..84a3cf9f5236daaee3b0a91274745127486a9c3d 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -25,18 +25,17 @@ 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
 
   end
 
 module NRKBO (B : Terms.Blob) : Blob 
-with type t = B.t and type input = B.input
+with type t = B.t 
 
 module KBO (B : Terms.Blob) : Blob 
-with type t = B.t and type input = B.input
+with type t = B.t 
 
-module LPO (B : Terms.Blob) : Blob 
-with type t = B.t and type input = B.input
+module LPO (B : Terms.Blob) : Blob
+with type t = B.t