coq 8.7.1 · OCaml Package

type level =
  Ppextend.precedence
  * Ppextend.tolerability list
  * Notation_term.notation_var_internalization_type list

type delimiters = string

type scope

type scopes

type local_scopes =
  Notation_term.tmp_scope_name option * Notation_term.scope_name list

val declare_scope : Notation_term.scope_name -> unit

val current_scopes : unit -> scopes

val level_eq : level -> level -> bool

val scope_is_open_in_scopes : Notation_term.scope_name -> scopes -> bool

val scope_is_open : Notation_term.scope_name -> bool

val open_close_scope : (bool * bool * Notation_term.scope_name) -> unit

val empty_scope_stack : scopes

val push_scope : Notation_term.scope_name -> scopes -> scopes

val find_scope : Notation_term.scope_name -> scope

val declare_delimiters : Notation_term.scope_name -> delimiters -> unit

val remove_delimiters : Notation_term.scope_name -> unit

val find_delimiters_scope : 
  ?loc:Loc.t ->
  delimiters ->
  Notation_term.scope_name

type notation_location = (Names.DirPath.t * Names.DirPath.t) * string

type required_module = Libnames.full_path * string list

type cases_pattern_status = bool

type !'a prim_token_interpreter = ?loc:Loc.t -> 'a -> Glob_term.glob_constr

type !'a prim_token_uninterpreter =
  Glob_term.glob_constr list
  * (Glob_term.glob_constr ->
  'a option)
  * cases_pattern_status

type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign

val declare_rawnumeral_interpreter : 
  Notation_term.scope_name ->
  required_module ->
  rawnum prim_token_interpreter ->
  rawnum prim_token_uninterpreter ->
  unit

val declare_numeral_interpreter : 
  Notation_term.scope_name ->
  required_module ->
  Bigint.bigint prim_token_interpreter ->
  Bigint.bigint prim_token_uninterpreter ->
  unit

val declare_string_interpreter : 
  Notation_term.scope_name ->
  required_module ->
  string prim_token_interpreter ->
  string prim_token_uninterpreter ->
  unit

val interp_prim_token : 
  ?loc:Loc.t ->
  Constrexpr.prim_token ->
  local_scopes ->
  Glob_term.glob_constr * (notation_location * Notation_term.scope_name option)

val interp_prim_token_cases_pattern_expr : 
  ?loc:Loc.t ->
  (Globnames.global_reference -> unit) ->
  Constrexpr.prim_token ->
  local_scopes ->
  Glob_term.glob_constr * (notation_location * Notation_term.scope_name option)

val uninterp_prim_token : 
  Glob_term.glob_constr ->
  Notation_term.scope_name * Constrexpr.prim_token

val uninterp_prim_token_cases_pattern : 
  Glob_term.cases_pattern ->
  Names.Name.t * Notation_term.scope_name * Constrexpr.prim_token

val uninterp_prim_token_ind_pattern : 
  Names.inductive ->
  Glob_term.cases_pattern list ->
  Notation_term.scope_name * Constrexpr.prim_token

val availability_of_prim_token : 
  Constrexpr.prim_token ->
  Notation_term.scope_name ->
  local_scopes ->
  delimiters option option

type interp_rule =

| NotationRule of Notation_term.scope_name option * Constrexpr.notation
| SynDefRule of Names.kernel_name

val declare_notation_interpretation : 
  Constrexpr.notation ->
  Notation_term.scope_name option ->
  Notation_term.interpretation ->
  notation_location ->
  onlyprint:bool ->
  unit

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

val interp_notation : 
  ?loc:Loc.t ->
  Constrexpr.notation ->
  local_scopes ->
  Notation_term.interpretation
  * (notation_location * Notation_term.scope_name option)

type notation_rule = interp_rule * Notation_term.interpretation * int option

val uninterp_notations : Glob_term.glob_constr -> notation_rule list

val uninterp_cases_pattern_notations : 
  Glob_term.cases_pattern ->
  notation_rule list

val uninterp_ind_pattern_notations : Names.inductive -> notation_rule list

val availability_of_notation : 
  (Notation_term.scope_name option * Constrexpr.notation) ->
  local_scopes ->
  (Notation_term.scope_name option * delimiters option) option

val declare_notation_level : Constrexpr.notation -> level -> unit

val level_of_notation : Constrexpr.notation -> level

val interp_notation_as_global_reference : 
  ?loc:Loc.t ->
  (Globnames.global_reference -> bool) ->
  Constrexpr.notation ->
  delimiters option ->
  Globnames.global_reference

val exists_notation_in_scope : 
  Notation_term.scope_name option ->
  Constrexpr.notation ->
  bool ->
  Notation_term.interpretation ->
  bool

val declare_arguments_scope : 
  bool ->
  Globnames.global_reference ->
  Notation_term.scope_name option list ->
  unit

val find_arguments_scope : 
  Globnames.global_reference ->
  Notation_term.scope_name option list

type scope_class

val scope_class_compare : scope_class -> scope_class -> int

val subst_scope_class : 
  Mod_subst.substitution ->
  scope_class ->
  scope_class option

val declare_scope_class : Notation_term.scope_name -> scope_class -> unit

val declare_ref_arguments_scope : Globnames.global_reference -> unit

val compute_arguments_scope : 
  Term.types ->
  Notation_term.scope_name option list

val compute_type_scope : Term.types -> Notation_term.scope_name option

val current_type_scope_name : unit -> Notation_term.scope_name option

val scope_class_of_class : Classops.cl_typ -> scope_class

type symbol =

| Terminal of string
| NonTerminal of Names.Id.t
| SProdList of Names.Id.t * symbol list
| Break of int

val symbol_eq : symbol -> symbol -> bool

val make_notation_key : symbol list -> Constrexpr.notation

val decompose_notation_key : Constrexpr.notation -> symbol list

val pr_scope_class : scope_class -> Pp.std_ppcmds

val pr_scope : 
  (Glob_term.glob_constr -> Pp.std_ppcmds) ->
  Notation_term.scope_name ->
  Pp.std_ppcmds

val pr_scopes : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Pp.std_ppcmds

val locate_notation : 
  (Glob_term.glob_constr -> Pp.std_ppcmds) ->
  Constrexpr.notation ->
  Notation_term.scope_name option ->
  Pp.std_ppcmds

val pr_visibility : 
  (Glob_term.glob_constr -> Pp.std_ppcmds) ->
  Notation_term.scope_name option ->
  Pp.std_ppcmds

type unparsing_rule = Ppextend.unparsing list * Ppextend.precedence

type extra_unparsing_rules = (string * string) list

val declare_notation_rule : 
  Constrexpr.notation ->
  extra:extra_unparsing_rules ->
  unparsing_rule ->
  Notation_term.notation_grammar ->
  unit

val find_notation_printing_rule : Constrexpr.notation -> unparsing_rule

val find_notation_extra_printing_rules : 
  Constrexpr.notation ->
  extra_unparsing_rules

val find_notation_parsing_rules : 
  Constrexpr.notation ->
  Notation_term.notation_grammar

val add_notation_extra_printing_rule : 
  Constrexpr.notation ->
  string ->
  string ->
  unit

val get_defined_notations : unit -> Constrexpr.notation list

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

package coq