better type for comparison and implementation of KBO orderings

[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 9d0f47d22d5f8de288735614e70607f5dd84638b..c7f67aa09313fb1ec9127856ec9f8d06b7c3338e 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -11,3 +11,16 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+module Orderings (B : Terms.Blob) :
+  sig 
+
+    (* This order relation should be:
+     * - stable for instantiation
+     * - total on ground terms
+     *
+     * The output can range only on Eq, Lt, Gt, Incomparable
+     *)
+    val compare_terms : 
+          B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
+
+  end