Lines Matching refs:Error
105 val () = assert (x = y) (Error "dest_refl")
118 val () = assert (x <> y) (Error "psym: refl")
155 if l = r then raise Error "term_order: refl"
162 | f (Pred x) (Eq y) = raise Error "obj_order: Pred > Eq"
195 raise Error "consistent: inconsistent orderings");
232 val () = assert (#term_order parm) (Error "dest_rewr: no rewrs")
234 val () = assert (x <> y) (Error "dest_rewr: refl")
268 fun fail _ = raise Error "gen_largest_lits: fail";
416 | _ => raise Error "match_occurs: not a variable"
417 val () = assert (not (mem v (FVT r))) (Error "match_occurs")
426 val () = assert (l <> r) (Error "dest_neq: reflexive")
440 handle Error _ => raise Bug "NEQ_VARS: shouldn't fail";
473 handle Error _ => raise Bug "mlibClause.REWRITE: shouldn't fail";
485 handle Error _ => raise Bug "mlibClause.QREWRITE: shouldn't fail";
561 (Error "assimilate: already included")
581 val () = assert (List.all (not o is_refl) lits) (Error "final: refl")
583 val () = assert (is_new hits acc) (Error "final: already seen")
641 handle Error _ => raise Bug "mlibClause.FACTOR: shouldn't fail";
682 handle e as Error _ => (p (INR (report e)); raise e)
716 handle Error _ => raise Bug "PARAMODULATE (rule): shouldn't fail"
731 handle e as Error _ => (p (INR (report e)); raise e)