ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_notation / grafiteAstPp.mli

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.mli b/helm/ocaml/cic_notation/grafiteAstPp.mli
index ad6c26db1a5779b9eb6c6971ff64535b3defc038..b8445095ff32ada3dcb419dab62d0920ce8f4f8b 100644 (file)
--- 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
+