X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.ml;h=3179f000068897755b450fcc8c315cc051c597ce;hb=a425ea9290454065cf33d33f0ae13a1006fef5fd;hp=5c085c5188db5a4473337995e167d17b290f5bfe;hpb=50ed5ab75a38693c7b7558ca9487998e81bb7f89;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 5c085c518..3179f0000 100644
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -93,11 +93,11 @@ module Index(B : Orderings.Blob) = struct
     | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> 
           DT.index t r (Terms.Right2Left, c)
     | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
-	if are_invertible maxvar vl l r then
+(*	if are_invertible maxvar vl l r then
 	  (prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^
 	     (Pp.pp_foterm r));
            DT.index t l (Terms.Left2Right, c))
-	   else
+	   else *)
           DT.index  
            (DT.index t l (Terms.Left2Right, c))
            r (Terms.Right2Left, c)