From 57e9e88aa1340997956b1e96ce7d470417a21412 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Jul 2009 10:01:23 +0000 Subject: [PATCH] two cases should be assert false at least in TPTP --- helm/software/components/ng_paramodulation/orderings.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2