HUGE COMMIT:

[helm.git] / matita / components / content / notationPp.mli

diff --git a/matita/components/content/notationPp.mli b/matita/components/content/notationPp.mli
index 51a284e2ef0872cb211ae5777af0794e881c9434..b1a5523329fe7b82592055d419c730fbf6ad669a 100644 (file)
--- a/matita/components/content/notationPp.mli
+++ b/matita/components/content/notationPp.mli
@@ -38,11 +38,11 @@
  * BoxPp.render_to_string(s)
  *)
 
-val pp_term: NotationPt.term -> string
+val pp_term: #NCic.status -> NotationPt.term -> string
 val pp_obj: ('term -> string) -> 'term NotationPt.obj -> string
 
-val pp_env: NotationEnv.t -> string
-val pp_value: NotationEnv.value -> string
+val pp_env: #NCic.status -> NotationEnv.t -> string
+val pp_value: #NCic.status -> NotationEnv.value -> string
 val pp_value_type: NotationEnv.value_type -> string
 
 val pp_pos: NotationPt.child_pos -> string
@@ -51,5 +51,4 @@ val pp_attribute: NotationPt.term_attribute -> string
 val pp_cic_appl_pattern: NotationPt.cic_appl_pattern -> string
 
  (** non re-entrant change of pp_term function above *)
-val set_pp_term: (NotationPt.term -> string) -> unit
-
+val set_pp_term: (NCic.status -> NotationPt.term -> string) -> unit