X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteAstPp.mli;h=b8445095ff32ada3dcb419dab62d0920ce8f4f8b;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=9268ea25bf1c475ac2032c2fdd48fc1cab64b9fa;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteAstPp.mli b/helm/ocaml/cic_notation/grafiteAstPp.mli
index 9268ea25b..b8445095f 100644
--- a/helm/ocaml/cic_notation/grafiteAstPp.mli
+++ b/helm/ocaml/cic_notation/grafiteAstPp.mli
@@ -23,17 +23,47 @@
  * http://helm.cs.unibo.it/
  *)
 
-val pp_tactic: (CicNotationPt.term, string) GrafiteAst.tactic -> string
+val pp_tactic:
+  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string)
+  GrafiteAst.tactic ->
+    string
+
 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: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.comment -> string
-val pp_executable: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.code -> string
-val pp_statement: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.statement -> string
+
+val pp_comment:
+  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj,
+   string)
+  GrafiteAst.comment ->
+    string
+
+val pp_executable:
+  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj,
+   string)
+  GrafiteAst.code ->
+    string
+
+val pp_statement:
+  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj,
+   string)
+  GrafiteAst.statement ->
+    string
+
 val pp_macro_ast: CicNotationPt.term GrafiteAst.macro -> string
 val pp_macro_cic: Cic.term GrafiteAst.macro -> string
-val pp_tactical: (CicNotationPt.term, string) GrafiteAst.tactical -> string
+
+val pp_tactical:
+  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string)
+  GrafiteAst.tactical ->
+    string
+
 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
+