Module Metasyntax

val add_token_obj : string -> unit
val add_infix : local:bool -> Deprecation.t option -> Environ.env -> (Names.lstring * Vernacexpr.syntax_modifier list) -> Constrexpr.constr_expr -> Notation_term.scope_name option -> unit
val add_notation : local:bool -> Deprecation.t option -> Environ.env -> Constrexpr.constr_expr -> (Names.lstring * Vernacexpr.syntax_modifier list) -> Notation_term.scope_name option -> unit
val add_notation_extra_printing_rule : string -> string -> string -> unit
val declare_scope : Vernacexpr.locality_flag -> Notation_term.scope_name -> unit
val add_delimiters : Vernacexpr.locality_flag -> Notation_term.scope_name -> string -> unit
val remove_delimiters : Vernacexpr.locality_flag -> Notation_term.scope_name -> unit
val add_class_scope : Vernacexpr.locality_flag -> Notation_term.scope_name -> Notation.scope_class list -> unit
val add_notation_interpretation : Environ.env -> (Names.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) -> unit
val set_notation_for_interpretation : Environ.env -> Constrintern.internalization_env -> (Names.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) -> unit
val add_syntax_extension : local:bool -> (Names.lstring * Vernacexpr.syntax_modifier list) -> unit
val add_syntactic_definition : local:bool -> Deprecation.t option -> Environ.env -> Names.Id.t -> (Names.Id.t list * Constrexpr.constr_expr) -> Flags.compat_version option -> unit
val pr_grammar : string -> Pp.t
val pr_custom_grammar : string -> Pp.t
val check_infix_modifiers : Vernacexpr.syntax_modifier list -> unit
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
val declare_custom_entry : Vernacexpr.locality_flag -> string -> unit