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 -> Bigint.bigint 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 numeral_ty = {
  1. int : int_ty;
  2. decimal : Names.inductive;
  3. hexadecimal : Names.inductive;
  4. numeral : Names.inductive;
}
type target_kind =
  1. | Int of int_ty
  2. | UInt of int_ty
  3. | Z of z_pos_ty
  4. | Int63
  5. | Numeral of numeral_ty
  6. | DecimalInt of int_ty
  7. | DecimalUInt of int_ty
  8. | Decimal of numeral_ty
type string_target_kind =
  1. | ListByte
  2. | Byte
type option_kind =
  1. | Option
  2. | Direct
type !'target conversion_kind = 'target * option_kind
type (!'target, !'warning) prim_token_notation_obj = {
  1. to_kind : 'target conversion_kind;
  2. to_ty : Names.GlobRef.t;
  3. of_kind : 'target conversion_kind;
  4. of_ty : Names.GlobRef.t;
  5. ty_name : Libnames.qualid;
  6. warning : 'warning;
}
type numeral_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. | NumeralNotation of numeral_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 -> Bigint.bigint prim_token_interpreter -> (Glob_term.glob_constr list * Bigint.bigint 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
val declare_notation_interpretation : Constrexpr.notation -> Notation_term.scope_name option -> Notation_term.interpretation -> notation_location -> onlyprint:bool -> Deprecation.t option -> unit
val declare_uninterpretation : interp_rule -> Notation_term.interpretation -> 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 interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (Names.GlobRef.t -> bool) -> Constrexpr.notation_key -> delimiters option -> Names.GlobRef.t
val exists_notation_in_scope : Notation_term.scope_name option -> Constrexpr.notation -> bool -> Notation_term.interpretation -> bool
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 -> 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 : Bigint.bigint -> Uint63.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct