From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 4 Jun 2009 10:18:12 +0000 (+0000)
Subject: comments
X-Git-Tag: make_still_working~3923
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b4afece869ffd5e87bd9faca6f1bad765ae5756d;p=helm.git

comments
---

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