X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=ccd6bf2864b4650174313446b6e1809b6b76f517;hb=c6b50e06bd73a29501cafe599551db206193220b;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..ccd6bf286 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -18,7 +18,6 @@ module Orderings (B : Terms.Blob) : * - 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