Module Notationextern

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

Equality on interpretation.

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

Equality on notation_entry_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 : ?also_in_cases_pattern:bool -> interp_rule -> Notation_term.interpretation -> unit
type notation_applicative_status =
| AppBoundedNotation of int
| AppUnboundedNotation
| NotAppNotation
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 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