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 50b31317a614f74336d11c933096961658f73080..13b876bed792e977ba675c6c930fce2b88578c96 100644 (file)
--- 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