X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=ccd6bf2864b4650174313446b6e1809b6b76f517;hb=01b628fc79155f545b283c1d095d8a2ffe00e0a1;hp=f2f6a1678ba249bdadfc5d74cbfd41eb7ab659e2;hpb=6c4056ea40b96039f24eeda9a1e1900c95bad7c8;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index f2f6a1678..ccd6bf286 100644
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -13,5 +13,13 @@
 
 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