Cic.term and Cic.obj unused!

[helm.git] / matita / components / grafite / grafiteAstPp.mli

diff --git a/matita/components/grafite/grafiteAstPp.mli b/matita/components/grafite/grafiteAstPp.mli
index 4ae11a59b3fa64df67f46f150fd583fe300dac50..6594d2137ff70963139a9fd00c8bd5868aab046f 100644 (file)
--- a/matita/components/grafite/grafiteAstPp.mli
+++ b/matita/components/grafite/grafiteAstPp.mli
@@ -43,14 +43,7 @@ val pp_reduction_kind:
   'a GrafiteAst.reduction ->
     string
 
-val pp_command:
- term_pp:('term -> string) ->
-  obj_pp:('obj -> string) ->
-   ('term,'obj) GrafiteAst.command -> string
-val pp_macro: 
-  term_pp:('term -> string) -> 
-  lazy_term_pp:('lazy_term -> string) ->
-    ('term,'lazy_term) GrafiteAst.macro -> string
+val pp_command: GrafiteAst.command -> string
 val pp_comment:
   map_unicode_to_tex:bool ->
   term_pp:('term -> string) ->