X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Fpp.ml;h=3f2a5cecc82202cf444080629efa11c5dc1cb43c;hb=4154281937451b96f89f7b2c5d098193448c240f;hp=ddf5726c49d0f6b479958a4e48ca9f969440f30d;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_paramodulation/pp.ml b/matita/components/ng_paramodulation/pp.ml
index ddf5726c4..3f2a5cecc 100644
--- a/matita/components/ng_paramodulation/pp.ml
+++ b/matita/components/ng_paramodulation/pp.ml
@@ -11,6 +11,13 @@
 
 (* $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 *)
@@ -63,7 +70,7 @@ let pp_proof bag ~formatter:f p =
         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
@@ -80,13 +87,6 @@ let pp_proof bag ~formatter:f p =
     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 ;