X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoUnif.ml;h=0946873b9af5c11fea237022b2394a40393e3de6;hb=b266ed97b63400d62ab4ba6a4ebdfbc1d5b0c2bb;hp=427db4f95bfca6c911bb5b1f6d9cf5dd786430ef;hpb=2bcf927f58bac034b8758173cdbd16cb7475de36;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 427db4f95..0946873b9 100644
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -29,7 +29,7 @@ module Founif (B : Orderings.Blob) = struct
   module Subst = FoSubst 
   module U = FoUtils.Utils(B)
 
-  let unification vars locked_vars t1 t2 =
+  let unification (* vars *) locked_vars t1 t2 =
     let rec occurs_check subst what where =
       match where with
       | Terms.Var i when i = what -> true
@@ -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
@@ -106,5 +107,6 @@ module Founif (B : Orderings.Blob) = struct
     in
       equiv Subst.id_subst s t
 ;;
+	
 
 end