From 791b0dc201a023e772e4ba5c3da697c5ae271405 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 15 May 2012 13:14:17 +0000 Subject: [PATCH] Divergence during indexing fixed: (? t = t') was not recognized as too flexible. --- matita/components/ng_paramodulation/nCicParamod.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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) ;; -- 2.39.2