X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=7586d41ac6c611ea31dd9f0c0ee0fc59437ec347;hb=10a9a8c36ff36e6a53bda1ec3074cb2fac03da63;hp=59cfde124c3468adbbbc7d567fb02d53d4b88880;hpb=4aaab68e38ccafb352cc2b656e3ec3cf1ef33cab;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index 59cfde124..7586d41ac 100644
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -11,4 +11,18 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val compare_terms : 'a Terms.foterm -> 'a Terms.foterm -> Terms.comparison
+module Orderings (B : Terms.Blob) :
+  sig 
+
+    (* This order relation should be:
+     * - stable for instantiation
+     * - total on ground terms
+     *
+     *)
+    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