Reorganized foUtils, added Clauses module to avoid duplicate code around are_invertib...

[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 4b5e23a48d68ea3ab12196f8a641057e28f67253..87792ec8c6faafd24f6b69dfc30f2094d7e226f6 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.mli
+++ b/helm/software/components/ng_paramodulation/foUnif.mli
@@ -13,12 +13,12 @@
 
 exception UnificationFailure of string Lazy.t;;
 
-module Founif (B : Terms.Blob) : 
+module FoUnif (B : Terms.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 ->