X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2FnCicParamod.ml;h=f56ac0cdf270e0bd567d1987746ea60421fbee1b;hb=9d2ded02c4252d3db0a9f5249d5b5d0f84f48d04;hp=9a8473f74a1b4c10b1750e28a686a1a36287b267;hpb=4c2b24a41bec48da2f6b5abc0dda537f12578a87;p=helm.git

diff --git a/matita/components/ng_paramodulation/nCicParamod.ml b/matita/components/ng_paramodulation/nCicParamod.ml
index 9a8473f74..f56ac0cdf 100644
--- a/matita/components/ng_paramodulation/nCicParamod.ml
+++ b/matita/components/ng_paramodulation/nCicParamod.ml
@@ -126,8 +126,8 @@ let tooflex (_,l,_,_) =
   match l with
     | Terms.Equation (l,r,_,o) ->
       (match l,r,o with
-       | Terms.Var _, _, (Terms.Incomparable | Terms.Invertible) -> true
-       | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) -> true
+       | (Terms.Var _ | Terms.Node (Terms.Var _::_)), _, (Terms.Incomparable | Terms.Invertible) -> true
+       | _, (Terms.Var _ | Terms.Node (Terms.Var _::_)),(Terms.Incomparable | Terms.Invertible) -> true
        | _ -> false)
     | _ -> false
 ;;  
@@ -142,8 +142,9 @@ let forward_infer_step status metasenv subst context s t ty =
   else
   let bag,clause = P.mk_passive bag (t,ty) in
     if Terms.is_eq_clause clause then
-      if tooflex clause then (print (lazy "pruning tooflex"); s)
-      else P.forward_infer_step (P.replace_bag s bag) clause 0
+      if tooflex clause then (debug (lazy "pruning tooflex"); s)
+      else
+       P.forward_infer_step (P.replace_bag s bag) clause 0
     else (debug (lazy "not eq"); s)
 ;;