Metasyntax
This data type packages all the necessary information to declare a notation interpretation, once the syntax is declared or recovered from a previous declaration.
val add_notation_syntax : local:bool -> infix:bool -> UserWarn.t option -> Vernacexpr.notation_declaration -> notation_interpretation_decl
Add syntax rules for a (constr) notation in the environment
val add_notation_interpretation : local:bool -> Environ.env -> notation_interpretation_decl -> unit
Declare the interpretation of a notation
Declaring scopes, delimiter keys and default scopes
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.add_scope_where option -> Notation.scope_class list -> unit
Scope opening
val open_close_scope : Vernacexpr.locality_flag -> to_open:bool -> Notation_term.scope_name -> unit
Add a notation interpretation associated to a "where" clause (already has pa/pp rules)
val prepare_where_notation : Vernacexpr.notation_declaration -> notation_interpretation_decl
Interpret the modifiers of a where-notation
val set_notation_for_interpretation : Environ.env -> Constrintern.internalization_env -> notation_interpretation_decl -> unit
Set the interpretation of the where-notation for interpreting a mutual block
Add only the parsing/printing rule of a notation
val add_reserved_notation : local:bool -> infix:bool -> (Names.lstring * Vernacexpr.syntax_modifier CAst.t list) -> unit
Add a syntactic definition (as in "Notation f := ...")
val add_abbreviation : local:bool -> Globnames.extended_global_reference UserWarn.with_qf option -> Environ.env -> Names.Id.t -> (Names.Id.t list * Constrexpr.constr_expr) -> Vernacexpr.syntax_modifier CAst.t list -> unit
Print the Camlp5 state of a grammar
val pr_grammar : string list -> Pp.t
val pr_custom_grammar : Libnames.qualid -> Pp.t
val pr_keywords : unit -> Pp.t
val declare_notation_toggle : Vernacexpr.locality_flag -> on:bool -> all:bool -> Notation.notation_query_pattern -> unit
val declare_custom_entry : Vernacexpr.locality_flag -> Names.Id.t -> unit
Declare given string as a custom grammar entry
val intern_custom_name : Libnames.qualid -> Globnames.CustomName.t
Intern custom entry name using compat layer if needed.
val intern_notation_entry : Libnames.qualid Constrexpr.notation_entry_gen -> Constrexpr.notation_entry
Intern notation entry name using compat layer for custom entries if needed.
val pr_level : (Constrexpr.notation_entry_level * Constrexpr.entry_relative_level list) -> Extend.constr_entry_key list -> Pp.t
Pretty print level information of a notation and all of its arguments