X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteAstPp.mli;h=b8445095ff32ada3dcb419dab62d0920ce8f4f8b;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ad6c26db1a5779b9eb6c6971ff64535b3defc038;hpb=d1126c6b78a3333bbf415daf027004496b77c2f4;p=helm.git diff --git a/helm/ocaml/cic_notation/grafiteAstPp.mli b/helm/ocaml/cic_notation/grafiteAstPp.mli index ad6c26db1..b8445095f 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.mli +++ b/helm/ocaml/cic_notation/grafiteAstPp.mli @@ -30,6 +30,7 @@ val pp_tactic: val pp_obj: GrafiteAst.obj -> string val pp_command: (CicNotationPt.term,GrafiteAst.obj) GrafiteAst.command -> string +val pp_metadata: GrafiteAst.metadata -> string val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string val pp_comment: @@ -62,3 +63,7 @@ val pp_alias: GrafiteAst.alias_spec -> string val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string +val pp_dependency: GrafiteAst.dependency -> string + +val pp_cic_appl_pattern: CicNotationPt.cic_appl_pattern -> string +