X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=ccd6bf2864b4650174313446b6e1809b6b76f517;hb=01b628fc79155f545b283c1d095d8a2ffe00e0a1;hp=74989c3ebaae8872686ef6a7cfe1e09d9492c80c;hpb=3c1a432c1612f8ed21f5b2220005599c4d9da1d5;p=helm.git diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli index 74989c3eb..ccd6bf286 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -17,6 +17,7 @@ module Orderings (B : Terms.Blob) : (* 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