X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoUnif.mli;h=6d50f70ee2339087099df6da70d9540a044b59a4;hb=fedc77dd81516395106ad70468dc1045b5b69263;hp=fc682c5fc102849d4932097f73aa9f0e0d02f52e;hpb=25cf2297c8d14c14cfb2ff7695c9b6331825f4c9;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli
index fc682c5fc..6d50f70ee 100644
--- a/helm/software/components/ng_paramodulation/foUnif.mli
+++ b/helm/software/components/ng_paramodulation/foUnif.mli
@@ -16,7 +16,7 @@ exception UnificationFailure of string Lazy.t;;
 module Founif (B : Terms.Blob) : 
   sig
 
-   val unification: 
+   val unification:
      (* global varlist for both terms t1 and t2 *)
      Terms.varlist -> 
      (* locked variables: if equal to FV(t2) we match t1 with t2*)
@@ -25,4 +25,10 @@ module Founif (B : Terms.Blob) :
      B.t Terms.foterm ->
         B.t Terms.substitution * Terms.varlist
 
+
+   val alpha_eq:
+     B.t Terms.foterm ->
+     B.t Terms.foterm ->
+     B.t Terms.substitution
+
   end