profile most operations, do not return a filtered varlist in unif (useless and expensive)

[helm.git] / helm / software / components / ng_paramodulation / foUnif.mli

diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli
index fc682c5fc102849d4932097f73aa9f0e0d02f52e..4b5e23a48d68ea3ab12196f8a641057e28f67253 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.mli
+++ b/helm/software/components/ng_paramodulation/foUnif.mli
@@ -16,13 +16,19 @@ 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*)
      Terms.varlist -> 
      B.t Terms.foterm ->
      B.t Terms.foterm ->
-        B.t Terms.substitution * Terms.varlist
+        B.t Terms.substitution 
+
+
+   val alpha_eq:
+     B.t Terms.foterm ->
+     B.t Terms.foterm ->
+     B.t Terms.substitution
 
   end