]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/pp.mli
First compiling version
[helm.git] / helm / software / components / ng_paramodulation / pp.mli
index 9cdc7a7c18882059b4e6cc6262aeb640bfa2314a..df0c0d325edd264edd833f2e16dd213ee39bcd18 100644 (file)
@@ -17,7 +17,8 @@ module Pp (B : Terms.Blob) :
     val pp_foterm: B.t Terms.foterm -> string
     val pp_proof: B.t Terms.bag -> B.t Terms.proof -> string
     val pp_substitution: B.t Terms.substitution -> string
-    val pp_unit_clause: B.t Terms.unit_clause -> string
+    val pp_unit_clause: ?margin:int -> B.t Terms.unit_clause -> string
+    val pp_clause: ?margin:int -> B.t Terms.clause -> string
     val pp_bag: B.t Terms.bag -> string
 
   end