aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/esyntax.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/esyntax.mli')
-rw-r--r--parsing/esyntax.mli11
1 files changed, 0 insertions, 11 deletions
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
index d6a7f4468..0344a27e2 100644
--- a/parsing/esyntax.mli
+++ b/parsing/esyntax.mli
@@ -48,16 +48,5 @@ module Ppprim :
val declare_primitive_printer :
string -> scope_name -> primitive_printer -> unit
-(*
-val declare_infix_symbol : Libnames.section_path -> string -> unit
-*)
-
(* Generic printing functions *)
-(*
-val token_printer: std_printer -> std_printer
-*)
-(*
-val print_syntax_entry :
- string -> unparsing_subfunction -> Ast.env -> Ast.astpat syntax_entry -> std_ppcmds
-*)
val genprint : std_printer -> unparsing_subfunction