the prover is almost OK, types in fuctors a bit extended to

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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index e931423b96b9d011965f13e8b1487e54c9c8c52b..3957e925e469d895f08ba866517e8a89497e54a3 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -178,11 +178,12 @@ module Superposition (B : Terms.Blob) =
     ;;
 
     (* move away *)
-    let is_identity_clause = function
+    let is_identity_clause ~unify = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
-      | _, Terms.Equation (l,r,_,_), vl, proof ->
+      | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
          (try ignore(Unif.unification vl [] l r); true
          with FoUnif.UnificationFailure _ -> false)
+      | _, Terms.Equation (_,_,_,_), _, _ -> false
       | _, Terms.Predicate _, _, _ -> assert false       
     ;;
 
@@ -404,7 +405,7 @@ module Superposition (B : Terms.Blob) =
     (* this is like simplify but raises Success *)
     let simplify_goal maxvar table bag g_actives clause = 
       let bag, clause = demodulate bag clause table in
-      if (is_identity_clause clause)
+      if (is_identity_clause ~unify:true clause)
       then raise (Success (bag, maxvar, clause))
 (*
       else