Notationextern (rocq-runtime.Notationextern)

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

Equality on notation_entry.

val notation_entry_compare : 
  Constrexpr.notation_entry ->
  Constrexpr.notation_entry ->
  int

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 notation_compare : Constrexpr.notation -> Constrexpr.notation -> int

val specific_notation_compare : 
  Constrexpr.specific_notation ->
  Constrexpr.specific_notation ->
  int

val notation_binder_kind_eq : 
  Notation_term.notation_binder_kind ->
  Notation_term.notation_binder_kind ->
  bool

Equality on notation_binder_kind.

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 interp_rule =

Binds a notation in a given scope to an interpretation

val remove_uninterpretation : 
  Environ.env ->
  interp_rule ->
  Notation_term.interpretation ->
  unit

val declare_uninterpretation : 
  Environ.env ->
  interp_rule ->
  Notation_term.interpretation ->
  unit

type notation_applicative_status =

type notation_rule = {

}

val uninterp_notations : 
  Environ.env ->
  'a Glob_term.glob_constr_g ->
  notation_rule list

Return the possible notations for a given term

val uninterp_cases_pattern_notations : 
  Environ.env ->
  'a Glob_term.cases_pattern_g ->
  notation_rule list

val uninterp_ind_pattern_notations : 
  Environ.env ->
  Names.inductive ->
  notation_rule list

val with_notation_uninterpretation_protection : ('a -> 'b) -> 'a -> 'b

State protection

type notation_use =

Miscellaneous