From c3ef73856c5dac1d197c9d41dc61c4b2163ae354 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 15 May 2012 23:20:33 +0000 Subject: [PATCH] Pruning generalized from Vars to applied Vars. Assert false since it can happen (???) that an equation is oriented as ? M -> N :-( --- matita/components/ng_paramodulation/superposition.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/matita/components/ng_paramodulation/superposition.ml b/matita/components/ng_paramodulation/superposition.ml index 50b31317a..13b876bed 100644 --- a/matita/components/ng_paramodulation/superposition.ml +++ b/matita/components/ng_paramodulation/superposition.ml @@ -145,11 +145,13 @@ module Superposition (B : Orderings.Blob) = (* CSC: to avoid equations of the form ? -> T that can always be applied and that lead to type-checking errors *) (match l,r,o with - Terms.Var _,_,Terms.Gt - | _,Terms.Var _,Terms.Lt -> assert false - | Terms.Var _,_,(Terms.Incomparable | Terms.Invertible) -> +(* + (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,Terms.Gt + | _,(Terms.Var _ | Terms.Node (Terms.Var _ ::_)),Terms.Lt -> assert false +*) + | (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,(Terms.Incomparable | Terms.Invertible) -> Terms.Equation (l, r, ty, Terms.Lt) - | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) -> + | _, (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),(Terms.Incomparable | Terms.Invertible) -> Terms.Equation (l, r, ty, Terms.Gt) | _ -> Terms.Equation (l, r, ty, o)) | t -> Terms.Predicate t -- 2.39.2