X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoUnif.mli;h=2371f2180c394cff4d3c19f57aca41c8ab38f2a8;hb=eeffdf0672400325577c1df83e10ad700b223262;hp=87b57ae70d74b979e83e021cfbae75a95941951e;hpb=b68e52f889215ce2c21c3d771f59b2d2057d53c1;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli
index 87b57ae70..2371f2180 100644
--- a/helm/software/components/ng_paramodulation/foUnif.mli
+++ b/helm/software/components/ng_paramodulation/foUnif.mli
@@ -17,8 +17,8 @@ module Founif (B : Orderings.Blob) :
   sig
 
    val unification:
-     (* global varlist for both terms t1 and t2 *)
-     Terms.varlist -> 
+     (* global varlist for both terms t1 and t2 (UNUSED) *)
+     (* Terms.varlist -> *)
      (* locked variables: if equal to FV(t2) we match t1 with t2*)
      Terms.varlist -> 
      B.t Terms.foterm ->