diff options
Diffstat (limited to 'parsing/esyntax.mli')
| -rw-r--r-- | parsing/esyntax.mli | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli index 40c541889..5ddadb5bc 100644 --- a/parsing/esyntax.mli +++ b/parsing/esyntax.mli @@ -11,6 +11,7 @@ (*i*) open Pp open Extend +open Vernacexpr (*i*) (* Syntax entry tables. *) @@ -24,9 +25,9 @@ val unfreeze : frozen_t -> unit (* Search and add a PP rule for an ast in the summary *) val find_syntax_entry : - string -> Coqast.t -> (syntax_entry * Ast.env) option -val add_rule : string -> syntax_entry -> unit -val add_ppobject : syntax_command -> unit + string -> Coqast.t -> (Ast.astpat syntax_entry * Ast.env) option +val add_rule : string -> Ast.astpat syntax_entry -> unit +val add_ppobject : Ast.astpat syntax_command -> unit val warning_verbose : bool ref (* Pretty-printing *) @@ -34,15 +35,17 @@ val warning_verbose : bool ref type std_printer = Coqast.t -> std_ppcmds type unparsing_subfunction = string -> tolerability option -> std_printer -(* Module of primitive printers *) +(* Module of constr primitive printers *) module Ppprim : sig type t = std_printer -> std_printer val add : string * t -> unit end +val declare_infix_symbol : Names.section_path -> string -> unit + (* Generic printing functions *) val token_printer: std_printer -> std_printer val print_syntax_entry : - string -> unparsing_subfunction -> Ast.env -> syntax_entry -> std_ppcmds + string -> unparsing_subfunction -> Ast.env -> Ast.astpat syntax_entry -> std_ppcmds val genprint : std_printer -> unparsing_subfunction |