X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=13b876bed792e977ba675c6c930fce2b88578c96;hb=5431da8145e4a84596d312fc02b552881d119100;hp=50b31317a614f74336d11c933096961658f73080;hpb=b78de5584633b864248519d9f7cd9f86a0005c24;p=helm.git

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