Compare was not compatible with eq!

[helm.git] / matita / components / ng_paramodulation / nCicParamod.ml

diff --git a/matita/components/ng_paramodulation/nCicParamod.ml b/matita/components/ng_paramodulation/nCicParamod.ml
index 9a8473f74a1b4c10b1750e28a686a1a36287b267..f56ac0cdf270e0bd567d1987746ea60421fbee1b 100644 (file)
--- 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)
 ;;