let symbols_counter = ref 0;;
(* non-recursive Knuth-Bendix term ordering by default *)
-Utils.compare_terms := Utils.nonrec_kbo;;
+(* Utils.compare_terms := Utils.nonrec_kbo;; *)
+Utils.compare_terms := Utils.ao;;
(* statistics... *)
let derived_clauses = ref 0;;
(* Negatives aren't indexed, no need to remove them... *)
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
- | [], hd::tl ->
+ | [], (hd:EqualitySet.elt)::tl ->
let passive_table =
Indexing.remove_index passive_table hd
in