Module `Notationextern`

Declaration of uninterpretation functions (i.e. printing rules) for notations

val notation_entry_eq : Constrexpr.notation_entry -> Constrexpr.notation_entry -> bool: Equality on notation_entry.

val notation_with_optional_scope_eq : Constrexpr.notation_with_optional_scope -> Constrexpr.notation_with_optional_scope -> bool
val notation_eq : Constrexpr.notation -> Constrexpr.notation -> bool: Equality on notation.

val interpretation_eq : Notation_term.interpretation -> Notation_term.interpretation -> bool: Equality on interpretation.

val notation_entry_level_eq : Constrexpr.notation_entry_level -> Constrexpr.notation_entry_level -> bool: Equality on notation_entry_level.

val notation_entry_relative_level_eq : Constrexpr.notation_entry_relative_level -> Constrexpr.notation_entry_relative_level -> bool: Equality on notation_entry_relative_level.

type level = Constrexpr.notation_entry_level * Constrexpr.entry_relative_level list: The "signature" of a rule: its level together with the levels of its subentries

val level_eq : level -> level -> bool: Equality on level.

val entry_relative_level_eq : Constrexpr.entry_relative_level -> Constrexpr.entry_relative_level -> bool: Equality on entry_relative_level.

type 'a interp_rule_gen = | NotationRule of Constrexpr.specific_notation | AbbrevRule of 'a: Binds a notation in a given scope to an interpretation

type interp_rule = Names.KerName.t interp_rule_gen

val remove_uninterpretation : interp_rule -> Notation_term.interpretation -> unit
val declare_uninterpretation : interp_rule -> Notation_term.interpretation -> unit

type notation_applicative_status = | AppBoundedNotation of int | AppUnboundedNotation | NotAppNotation
type notation_rule = interp_rule * Notation_term.interpretation * notation_applicative_status
type key: Return printing key

val glob_prim_constr_key : 'a Glob_term.glob_constr_g -> Names.GlobRef.t option
val glob_constr_keys : Glob_term.glob_constr -> key list
val cases_pattern_key : Glob_term.cases_pattern -> key
val notation_constr_key : Notation_term.notation_constr -> key * notation_applicative_status
val uninterp_notations : 'a Glob_term.glob_constr_g -> notation_rule list: Return the possible notations for a given term

val uninterp_cases_pattern_notations : 'a Glob_term.cases_pattern_g -> notation_rule list
val uninterp_ind_pattern_notations : Names.inductive -> notation_rule list
val with_notation_uninterpretation_protection : ('a -> 'b) -> 'a -> 'b: State protection

type notation_use = | OnlyPrinting | OnlyParsing | ParsingAndPrinting: Miscellaneous