...

[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 84de696df9f088f3c0e7cbc4a244e86952355176..d3e6000b77781dd88758678eb7d63364f83c7740 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -15,7 +15,7 @@ module Superposition (B : Terms.Blob) =
   struct
     module IDX = Index.Index(B)
     module Unif = FoUnif.Founif(B)
-    module Subst = FoSubst (*.Subst(B)*)
+    module Subst = FoSubst 
     module Order = Orderings.Orderings(B)
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
@@ -133,7 +133,6 @@ module Superposition (B : Terms.Blob) =
     ;;
 
     let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table =
-      (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*)
       match literal with
       | Terms.Predicate t -> assert false
       | Terms.Equation (l,r,ty,_) ->