X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.mli;h=b1a5523329fe7b82592055d419c730fbf6ad669a;hb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;hp=51a284e2ef0872cb211ae5777af0794e881c9434;hpb=a4a2345e2efaf4cc64aa4daf40e2bce05a400f12;p=helm.git diff --git a/matita/components/content/notationPp.mli b/matita/components/content/notationPp.mli index 51a284e2e..b1a552332 100644 --- 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