NotationexternDeclaration of uninterpretation functions (i.e. printing rules) for notations
val notation_entry_eq :
Constrexpr.notation_entry ->
Constrexpr.notation_entry ->
boolEquality on notation_entry.
val notation_with_optional_scope_eq :
Constrexpr.notation_with_optional_scope ->
Constrexpr.notation_with_optional_scope ->
boolval notation_eq : Constrexpr.notation -> Constrexpr.notation -> boolEquality on notation.
val interpretation_eq :
Notation_term.interpretation ->
Notation_term.interpretation ->
boolEquality on interpretation.
val notation_entry_level_eq :
Constrexpr.notation_entry_level ->
Constrexpr.notation_entry_level ->
boolEquality on notation_entry_level.
type level =
Constrexpr.notation_entry
* Constrexpr.entry_level
* Constrexpr.entry_relative_level listval entry_relative_level_eq :
Constrexpr.entry_relative_level ->
Constrexpr.entry_relative_level ->
boolEquality on entry_relative_level.
Binds a notation in a given scope to an interpretation
type interp_rule = Names.KerName.t interp_rule_genval remove_uninterpretation :
interp_rule ->
Notation_term.interpretation ->
unitval declare_uninterpretation :
?also_in_cases_pattern:bool ->
interp_rule ->
Notation_term.interpretation ->
unittype notation_rule =
interp_rule * Notation_term.interpretation * notation_applicative_statusval glob_prim_constr_key : 'a Glob_term.glob_constr_g -> Names.GlobRef.t optionval glob_constr_keys : Glob_term.glob_constr -> key listval cases_pattern_key : Glob_term.cases_pattern -> keyval notation_constr_key :
Notation_term.notation_constr ->
key * notation_applicative_statusval uninterp_notations : 'a Glob_term.glob_constr_g -> notation_rule listReturn the possible notations for a given term
val uninterp_cases_pattern_notations :
'a Glob_term.cases_pattern_g ->
notation_rule listval uninterp_ind_pattern_notations : Names.inductive -> notation_rule list