1. matitaEngine splitted into disambiguation (now in grafite_parser) and

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

diff --git a/helm/ocaml/grafite/grafiteAstPp.mli b/helm/ocaml/grafite/grafiteAstPp.mli
index 79900a3427d248721b7a3208b9a06a68ec2871ec..eefcd9ccbbea325c3b6cc2904d85ef17163498f0 100644 (file)
--- a/helm/ocaml/grafite/grafiteAstPp.mli
+++ b/helm/ocaml/grafite/grafiteAstPp.mli
@@ -24,7 +24,7 @@
  *)
 
 val pp_tactic:
-  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string)
+  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
   GrafiteAst.tactic ->
     string
 
@@ -34,19 +34,19 @@ val pp_metadata: GrafiteAst.metadata -> string
 val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string
 
 val pp_comment:
-  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction,
+  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
    CicNotationPt.obj, string)
   GrafiteAst.comment ->
     string
 
 val pp_executable:
-  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction,
+  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
    CicNotationPt.obj, string)
   GrafiteAst.code ->
     string
 
 val pp_statement:
-  (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction,
+  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
    CicNotationPt.obj, string)
   GrafiteAst.statement ->
     string
@@ -55,7 +55,7 @@ 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, GrafiteAst.reduction, string)
+  (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
   GrafiteAst.tactical ->
     string