(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+let string_of_comparison = function
+ | Terms.Lt -> "=<="
+ | Terms.Gt -> "=>="
+ | Terms.Eq -> "==="
+ | Terms.Incomparable -> "=?="
+ | Terms.Invertible -> "=<->="
+
module Pp (B : Terms.Blob) = struct
(* Main pretty printing functions *)
Format.fprintf f "%d: Exact (" eq;
pp_foterm f t;
Format.fprintf f ")@;";
- | Terms.Step (rule,eq1,eq2,dir,pos,subst) ->
+ | Terms.Step (rule,eq1,eq2,dir,_pos,_subst) ->
Format.fprintf f "%d: %s("
eq (string_of_rule rule);
Format.fprintf f "|%d with %d dir %s))" eq1 eq2
Format.fprintf f "@]"
;;
-let string_of_comparison = function
- | Terms.Lt -> "=<="
- | Terms.Gt -> "=>="
- | Terms.Eq -> "==="
- | Terms.Incomparable -> "=?="
- | Terms.Invertible -> "=<->="
-
let pp_unit_clause ~formatter:f c =
let (id, l, vars, proof) = c in
Format.fprintf f "Id : %3d, " id ;