profile most operations, do not return a filtered varlist in unif (useless and expensive)

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

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 454432ec48925a4e53dc734aa6680faff7e14d7f..10c96f543578f2133898f2077323f85cc1483855 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -72,15 +72,15 @@ module Utils (B : Terms.Blob) = struct
   let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2
   let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2
     
-  let relocate maxvar varlist =
+  let relocate maxvar varlist subst =
     List.fold_right
       (fun i (maxvar, varlist, s) -> 
          maxvar+1, maxvar::varlist, Subst.build_subst i (Terms.Var maxvar) s)
-      varlist (maxvar+1, [], Subst.id_subst)
+      varlist (maxvar+1, [], subst)
   ;;
 
   let fresh_unit_clause maxvar (id, lit, varlist, proof) =
-    let maxvar, varlist, subst = relocate maxvar varlist in
+    let maxvar, varlist, subst = relocate maxvar varlist Subst.id_subst in
     let lit = 
       match lit with
       | Terms.Equation (l,r,ty,o) ->