X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=74989c3ebaae8872686ef6a7cfe1e09d9492c80c;hb=6b0a195b180e3526af7b55771b2df7b10acd7c30;hp=c7f67aa09313fb1ec9127856ec9f8d06b7c3338e;hpb=b60b04a930b208dc0bf8876305c4fa5ea2aeb619;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index c7f67aa09..74989c3eb 100644
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -17,8 +17,6 @@ module Orderings (B : Terms.Blob) :
     (* 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