package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val pr_notation : Constrexpr.notation -> Pp.t
val notation_entry_eq : Constrexpr.notation_entry -> Constrexpr.notation_entry -> bool
val notation_entry_level_eq : Constrexpr.notation_entry_level -> Constrexpr.notation_entry_level -> bool
val notation_eq : Constrexpr.notation -> Constrexpr.notation -> bool
module NotationSet : sig ... end
module NotationMap : sig ... end
module SpecificNotationSet : sig ... end
module SpecificNotationMap : sig ... end
type delimiters = string
type scope
type scopes
val declare_scope : Notation_term.scope_name -> unit
val ensure_scope : Notation_term.scope_name -> unit
val current_scopes : unit -> scopes
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 rawnum = NumTok.Signed.t
type prim_token_uid = string
type !'a prim_token_interpreter = ?loc:Loc.t -> 'a -> Glob_term.glob_constr
type !'a prim_token_uninterpreter = Glob_term.any_glob_constr -> 'a option
type !'a prim_token_interpretation = 'a prim_token_interpreter * 'a prim_token_uninterpreter
val register_rawnumeral_interpretation : ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
val register_bignumeral_interpretation : ?allow_overwrite:bool -> prim_token_uid -> Z.t prim_token_interpretation -> unit
val register_string_interpretation : ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
type prim_token_notation_error =
  1. | UnexpectedTerm of Constr.t
  2. | UnexpectedNonOptionTerm of Constr.t
exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error
type numnot_option =
  1. | Nop
  2. | Warning of NumTok.UnsignedNat.t
  3. | Abstract of NumTok.UnsignedNat.t
type int_ty = {
  1. dec_uint : Names.inductive;
  2. dec_int : Names.inductive;
  3. hex_uint : Names.inductive;
  4. hex_int : Names.inductive;
  5. uint : Names.inductive;
  6. int : Names.inductive;
}
type z_pos_ty = {
  1. z_ty : Names.inductive;
  2. pos_ty : Names.inductive;
}
type number_ty = {
  1. int : int_ty;
  2. decimal : Names.inductive;
  3. hexadecimal : Names.inductive;
  4. number : Names.inductive;
}
type target_kind =
  1. | Int of int_ty
  2. | UInt of int_ty
  3. | Z of z_pos_ty
  4. | Int63
  5. | Number of number_ty
  6. | DecimalInt of int_ty
  7. | DecimalUInt of int_ty
  8. | Decimal of number_ty
type string_target_kind =
  1. | ListByte
  2. | Byte
type option_kind =
  1. | Option
  2. | Direct
type !'target conversion_kind = 'target * option_kind
type to_post_arg =
  1. | ToPostCopy
  2. | ToPostAs of int
  3. | ToPostHole
  4. | ToPostCheck of Names.GlobRef.t
type (!'target, !'warning) prim_token_notation_obj = {
  1. to_kind : 'target conversion_kind;
  2. to_ty : Names.GlobRef.t;
  3. to_post : (Names.GlobRef.t * Names.GlobRef.t * to_post_arg list) list array;
  4. of_kind : 'target conversion_kind;
  5. of_ty : Names.GlobRef.t;
  6. ty_name : Libnames.qualid;
  7. warning : 'warning;
}
type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
type prim_token_interp_info =
  1. | Uid of prim_token_uid
  2. | NumberNotation of number_notation_obj
  3. | StringNotation of string_notation_obj
type prim_token_infos = {
  1. pt_local : bool;
  2. pt_scope : Notation_term.scope_name;
  3. pt_interp_info : prim_token_interp_info;
  4. pt_required : required_module;
  5. pt_refs : Names.GlobRef.t list;
  6. pt_in_match : bool;
}
val enable_prim_token_interpretation : prim_token_infos -> unit
val declare_numeral_interpreter : ?local:bool -> Notation_term.scope_name -> required_module -> Z.t prim_token_interpreter -> (Glob_term.glob_constr list * Z.t prim_token_uninterpreter * bool) -> unit
val declare_string_interpreter : ?local:bool -> Notation_term.scope_name -> required_module -> string prim_token_interpreter -> (Glob_term.glob_constr list * string prim_token_uninterpreter * bool) -> unit
val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (Names.GlobRef.t -> unit) -> Constrexpr.prim_token -> Notation_term.subscopes -> Glob_term.glob_constr * (notation_location * Notation_term.scope_name option)
val uninterp_prim_token_cases_pattern : 'a Glob_term.cases_pattern_g -> Notation_term.subscopes -> Names.Name.t * Constrexpr.prim_token * delimiters option
val availability_of_prim_token : Constrexpr.prim_token -> Notation_term.scope_name -> Notation_term.subscopes -> delimiters option option
type interp_rule =
  1. | NotationRule of Constrexpr.specific_notation
  2. | SynDefRule of Names.KerName.t
type notation_use =
  1. | OnlyPrinting
  2. | OnlyParsing
  3. | ParsingAndPrinting
val declare_uninterpretation : ?also_in_cases_pattern:bool -> interp_rule -> Notation_term.interpretation -> unit
type entry_coercion_kind =
  1. | IsEntryCoercion of Constrexpr.notation_entry_level
  2. | IsEntryGlobal of string * int
  3. | IsEntryIdent of string * int
val declare_notation : (Constrexpr.notation_with_optional_scope * Constrexpr.notation) -> Notation_term.interpretation -> notation_location -> use:notation_use -> also_in_cases_pattern:bool -> entry_coercion_kind option -> Deprecation.t option -> unit
type notation_applicative_status =
  1. | AppBoundedNotation of int
  2. | AppUnboundedNotation
  3. | NotAppNotation
val uninterp_notations : 'a Glob_term.glob_constr_g -> notation_rule list
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 availability_of_notation : Constrexpr.specific_notation -> Notation_term.subscopes -> (Notation_term.scope_name option * delimiters option) option
val is_printing_inactive_rule : interp_rule -> Notation_term.interpretation -> bool
val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (Names.GlobRef.t -> bool) -> Constrexpr.notation_key -> delimiters option -> Names.GlobRef.t
val declare_arguments_scope : bool -> Names.GlobRef.t -> Notation_term.scope_name option list -> unit
val find_arguments_scope : Names.GlobRef.t -> Notation_term.scope_name option list
type scope_class
val scope_class_compare : scope_class -> scope_class -> int
val subst_scope_class : Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option
val declare_scope_class : Notation_term.scope_name -> scope_class -> unit
val declare_ref_arguments_scope : Evd.evar_map -> Names.GlobRef.t -> unit
val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> Notation_term.scope_name option list
val compute_type_scope : Environ.env -> Evd.evar_map -> EConstr.types -> Notation_term.scope_name option
val current_type_scope_name : unit -> Notation_term.scope_name option
val scope_class_of_class : Coercionops.cl_typ -> scope_class
type symbol =
  1. | Terminal of string
  2. | NonTerminal of Names.Id.t
  3. | SProdList of Names.Id.t * symbol list
  4. | Break of int
val symbol_eq : symbol -> symbol -> bool
val make_notation_key : Constrexpr.notation_entry -> symbol list -> Constrexpr.notation
val decompose_notation_key : Constrexpr.notation -> Constrexpr.notation_entry * symbol list
val decompose_raw_notation : string -> (Names.Id.t * Names.Id.t) list * Names.Id.t list * symbol list
val pr_scope_class : scope_class -> Pp.t
val pr_scopes : (Glob_term.glob_constr -> Pp.t) -> Pp.t
val pr_visibility : (Glob_term.glob_constr -> Pp.t) -> Notation_term.scope_name option -> Pp.t
val make_notation_entry_level : Constrexpr.notation_entry -> Constrexpr.entry_level -> Constrexpr.notation_entry_level
type entry_coercion = (Constrexpr.notation_with_optional_scope * Constrexpr.notation) list
val declare_entry_coercion : Constrexpr.specific_notation -> Constrexpr.entry_level option -> Constrexpr.notation_entry_level -> unit
val availability_of_entry_coercion : Constrexpr.notation_entry_level -> Constrexpr.notation_entry_level -> entry_coercion option
val declare_custom_entry_has_global : string -> int -> unit
val declare_custom_entry_has_ident : string -> int -> unit
val entry_has_global : Constrexpr.notation_entry_level -> bool
val entry_has_ident : Constrexpr.notation_entry_level -> bool
val level_eq : level -> level -> bool
val entry_relative_level_eq : Constrexpr.entry_relative_level -> Constrexpr.entry_relative_level -> bool
val declare_notation_level : Constrexpr.notation -> level -> unit
val level_of_notation : Constrexpr.notation -> level
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
val int63_of_pos_bigint : Z.t -> Uint63.t