X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FfoUnif.ml;h=61bbdcd8be9b7bf0ae76ac6311c108a0197a70b2;hb=39a2078b0e835d39895a5b6c0862d668ece544f3;hp=cb3045c1918e9b0c9682e68c939440eb061d5c10;hpb=95a14ced97592a4116485f94c6ffa806feb62dbc;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index cb3045c19..61bbdcd8b 100644
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -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