]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.mli
better nlet rec boxing
[helm.git] / helm / software / components / grafite / grafiteAstPp.mli
index 8f6904545d70e7c709f2a52d4be2ce68036efccc..4ae11a59b3fa64df67f46f150fd583fe300dac50 100644 (file)
@@ -78,10 +78,5 @@ val pp_statement:
   map_unicode_to_tex:bool ->
     string
 
-val pp_punctuation_tactical:
-  term_pp:('term -> string) ->
-  lazy_term_pp:('lazy_term -> string) ->
-  ('term, 'lazy_term, 'term GrafiteAst.reduction, string)
-  GrafiteAst.punctuation_tactical ->
-    string
+val pp_punctuation_tactical: GrafiteAst.punctuation_tactical -> string