X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fterms.mli;h=93f106a4f1c9e8c8464a1582a13d6d0a4c79d6c8;hb=e22808c929a9cebf5e4e2b7428ff0cbf89e1f92a;hp=03bdddb89fb55d94f500bfc7366c3f089e5a24a4;hpb=f7804325dbb5b51820edefe5d5ffff89809fe35c;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index 03bdddb89..93f106a4f 100644
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -87,6 +87,7 @@ module type Blob =
     (* TODO: consider taking in input an imperative buffer for Format 
      *  val pp : Format.formatter -> t -> unit
      * *)
+    val is_eq : t foterm -> (t foterm * t foterm * t foterm) option
     val pp : t -> string
 
     type input