more functors

[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 f2f6a1678ba249bdadfc5d74cbfd41eb7ab659e2..74989c3ebaae8872686ef6a7cfe1e09d9492c80c 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -13,5 +13,12 @@
 
 module Orderings (B : Terms.Blob) :
   sig 
-    val compare_terms : B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
+
+    (* 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
+
   end