From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Jul 2009 10:01:23 +0000 (+0000)
Subject: two cases should be assert false at least in TPTP
X-Git-Tag: make_still_working~3718
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=57e9e88aa1340997956b1e96ce7d470417a21412

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 28fbe1507..27b3ac647 100644
--- 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