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

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

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index cb3045c1918e9b0c9682e68c939440eb061d5c10..916e33ca83aa5d4039ab46ec279aecf35ae65707 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -25,7 +25,7 @@ let mem2 a b l =
    aux false false l
 ;;
 
-module Founif (B : Orderings.Blob) = struct
+module FoUnif (B : Terms.Blob) = struct
   module Subst = FoSubst 
   module U = FoUtils.Utils(B)
 
@@ -81,6 +81,7 @@ module Founif (B : Orderings.Blob) = struct
     subst
 ;;
 
+(* Sets of variables in s and t are assumed to be disjoint  *)
   let alpha_eq s t =
     let rec equiv subst s t =
       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s