functorial abstraction over term blobs

[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 46c588676628a7e5ffdb5d43fe349e497f8cc3e1..dbfca2073cc51ba82408c0410b98a915218e3082 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.mli
+++ b/helm/software/components/ng_paramodulation/pp.mli
@@ -11,9 +11,12 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val pp_foterm: ('a -> string) -> 'a Terms.foterm -> string
-val pp_proof: ('a -> string) -> 'a Terms.bag -> 'a Terms.proof -> string
-val pp_substitution: ('a -> string) -> 'a Terms.substitution -> string
-val pp_unit_clause: ('a -> string) -> 'a Terms.unit_clause -> string
+module Pp (B : Terms.Blob) : 
+  sig
 
+    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
 
+  end