Module `Metasyntax`

val add_notation : local:bool -> infix:bool -> Deprecation.t option -> Environ.env -> Constrexpr.constr_expr -> (Names.lstring * Vernacexpr.syntax_modifier CAst.t 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

type where_decl_notation

val prepare_where_notation : Vernacexpr.decl_notation -> where_decl_notation: Interpret the modifiers of a where-notation

val add_notation_interpretation : local:bool -> Environ.env -> where_decl_notation -> unit: Declare the interpretation of the where-notation

val set_notation_for_interpretation : Environ.env -> Constrintern.internalization_env -> where_decl_notation -> unit: Set the interpretation of the where-notation for interpreting a mutual block

val add_reserved_notation : local:bool -> infix:bool -> (Names.lstring * Vernacexpr.syntax_modifier CAst.t list) -> unit

val add_abbreviation : local:bool -> Deprecation.t option -> Environ.env -> Names.Id.t -> (Names.Id.t list * Constrexpr.constr_expr) -> Vernacexpr.syntax_modifier CAst.t list -> unit

val pr_grammar : string -> Pp.t
val pr_custom_grammar : string -> Pp.t
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
val declare_custom_entry : Vernacexpr.locality_flag -> string -> unit: Declare given string as a custom grammar entry

val check_custom_entry : string -> unit: Check that the given string is a valid custom entry that has been declared

val pr_level : Constrexpr.notation -> Notation.level -> Extend.constr_entry_key list -> Pp.t: Pretty print level information of a notation and all of its arguments