From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 15 May 2012 23:20:33 +0000 (+0000)
Subject: Pruning generalized from Vars to applied Vars.
X-Git-Tag: make_still_working~1736
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c3ef73856c5dac1d197c9d41dc61c4b2163ae354;p=helm.git

Pruning generalized from Vars to applied Vars.
Assert false since it can happen (???) that an equation
is oriented as ? M -> N   :-(
---

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