more functors

[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 bc18aaf00f3248dc715df19ff72d2b680b791e81..5a3f67ae90dd5f5000d0eb866661817b056e7c33 100644 (file)
--- a/helm/software/components/ng_paramodulation/founif.ml
+++ b/helm/software/components/ng_paramodulation/founif.ml
@@ -15,6 +15,7 @@ exception UnificationFailure of string Lazy.t;;
 
 module Founif (B : Terms.Blob) = struct
   module Subst = Subst.Subst(B)
+  module U = Terms.Utils(B)
 
   let unification vars locked_vars t1 t2 =
     let lookup = Subst.lookup_subst in
@@ -23,7 +24,7 @@ module Founif (B : Terms.Blob) = struct
       | Terms.Var i when i = what -> true
       | Terms.Var _ ->
           let t = lookup where subst in
-          if t <> where then occurs_check subst what t else false
+          if not (U.eq_foterm t where) then occurs_check subst what t else false
       | Terms.Node l -> List.exists (occurs_check subst what) l
       | _ -> false
     in
@@ -33,7 +34,7 @@ module Founif (B : Terms.Blob) = struct
       
       in
       match s, t with
-      | s, t when s = t -> subst, vars
+      | s, t when U.eq_foterm s t -> subst, vars
       | Terms.Var i, Terms.Var j
           when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
           raise
@@ -52,7 +53,7 @@ module Founif (B : Terms.Blob) = struct
           let subst = Subst.buildsubst i t subst in
           subst, vars
       | _, Terms.Var _ -> unif subst vars t s
-      | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt ->
+      | Terms.Node (hds::_),Terms.Node (hdt::_) when not(U.eq_foterm hds hdt)->
           raise (UnificationFailure (lazy "Inference.unification.unif"))
       | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
           try