From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 29 Jun 2009 14:44:21 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3771
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7f29d7713208180a1b09b3f903c1b5fd8ec4c896;p=helm.git

...
---

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 84de696df..d3e6000b7 100644
--- 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,_) ->