From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 15 May 2012 13:14:17 +0000 (+0000)
Subject: Divergence during indexing fixed: (? t = t') was not recognized as too flexible.
X-Git-Tag: make_still_working~1742
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=791b0dc201a023e772e4ba5c3da697c5ae271405;p=helm.git

Divergence during indexing fixed: (? t = t') was not recognized as too flexible.
---

diff --git a/matita/components/ng_paramodulation/nCicParamod.ml b/matita/components/ng_paramodulation/nCicParamod.ml
index 9a8473f74..a2cc88b5f 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
 ;;  
@@ -143,7 +143,8 @@ let forward_infer_step status metasenv subst context s t ty =
   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
+      else
+       P.forward_infer_step (P.replace_bag s bag) clause 0
     else (debug (lazy "not eq"); s)
 ;;