right inference step completed

[helm.git] / helm / software / components / ng_paramodulation / pp.mli

diff --git a/helm/software/components/ng_paramodulation/pp.mli b/helm/software/components/ng_paramodulation/pp.mli
index dbfca2073cc51ba82408c0410b98a915218e3082..9cdc7a7c18882059b4e6cc6262aeb640bfa2314a 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.mli
+++ b/helm/software/components/ng_paramodulation/pp.mli
@@ -18,5 +18,6 @@ module Pp (B : Terms.Blob) :
     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_bag: B.t Terms.bag -> string
 
   end