* http://helm.cs.unibo.it/
*)
+(** ZACK
+ * This module does not print terms and object properly, it has been created
+ * mainly for debugging reason. There is no guarantee that printed strings are
+ * re-parsable. Moreover, actually there is no way at all to proper print
+ * objects in a way that is re-parsable.
+ *
+ * TODO the proper implementation of a pp_obj function like the one below should
+ * be as follows. Change its type to
+ * pp_obj: CicNotationPt.obj -> CicNotationPres.markup
+ * and parametrize it over a function with the following type
+ * pp_term: CicNotationPt.term -> CicNotationPres.markup
+ * The obtained markup can then be printed using CicNotationPres.print_xml or
+ * BoxPp.render_to_string(s)
+ *)
+
val pp_term: CicNotationPt.term -> string
val pp_obj: CicNotationPt.obj -> string
val pp_cic_appl_pattern: CicNotationPt.cic_appl_pattern -> string
+ (** non re-entrant change of pp_term function above *)
+val set_pp_term: (CicNotationPt.term -> string) -> unit
+