X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite%2FgrafiteAstPp.mli;h=80d2174f70dff3512fc96b73dba4b5e475166a7d;hb=55ba0a660f91e491e904dad63b14ddf2bcc2754d;hp=eefcd9ccbbea325c3b6cc2904d85ef17163498f0;hpb=a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5;p=helm.git

diff --git a/helm/ocaml/grafite/grafiteAstPp.mli b/helm/ocaml/grafite/grafiteAstPp.mli
index eefcd9ccb..80d2174f7 100644
--- a/helm/ocaml/grafite/grafiteAstPp.mli
+++ b/helm/ocaml/grafite/grafiteAstPp.mli
@@ -24,44 +24,56 @@
  *)
 
 val pp_tactic:
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  ('term, 'lazy_term, 'term GrafiteAst.reduction, string)
   GrafiteAst.tactic ->
     string
 
-val pp_command:
-  (CicNotationPt.term,CicNotationPt.obj) GrafiteAst.command -> string
-val pp_metadata: GrafiteAst.metadata -> string
-val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string
+val pp_tactic_pattern:
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  ('term, 'lazy_term, string) GrafiteAst.pattern ->
+    string
+
+val pp_reduction_kind:
+  term_pp:('a -> string) ->
+  'a GrafiteAst.reduction ->
+    string
+
+val pp_command: obj_pp:('obj -> string) -> 'obj GrafiteAst.command -> string
+val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string
+val pp_alias: GrafiteAst.alias_spec -> string
+val pp_dependency:  GrafiteAst.dependency -> string
 
 val pp_comment:
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
-   CicNotationPt.obj, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  obj_pp:('obj -> string) ->
+  ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
   GrafiteAst.comment ->
     string
 
 val pp_executable:
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
-   CicNotationPt.obj, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  obj_pp:('obj -> string) ->
+  ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
   GrafiteAst.code ->
     string
 
 val pp_statement:
-  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
-   CicNotationPt.obj, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  obj_pp:('obj -> string) ->
+  ('term, 'lazy_term, 'term GrafiteAst.reduction, '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, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
+  term_pp:('term -> string) ->
+  lazy_term_pp:('lazy_term -> string) ->
+  ('term, 'lazy_term, '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
-