two cases should be assert false at least in TPTP

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 28fbe15073ae2fc32abf0dbfeda32e0e15726e2b..27b3ac6472395e9dda0d151cf032a6c4d81d5957 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -164,8 +164,8 @@ let compute_goal_weight (_,l, _, _) =
         let rec cmp t1 t2 =
           match t1, t2 with
           | [], [] -> XEQ
-          | _, [] -> XGT
-          | [], _ -> XLT
+          | _, [] -> (* XGT *) assert false (* hd symbols were eq *)
+          | [], _ -> (* XLT *) assert false (* hd symbols were eq *)
           | hd1::tl1, hd2::tl2 ->
               let o = aux_ordering ~head_only hd1 hd2 in
               if o = XEQ && not head_only then cmp tl1 tl2 else o