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
type delimiters = string
type scope
type scopes
val declare_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 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 numeral_notation_error =
  1. | UnexpectedTerm of Constr.t
  2. | UnexpectedNonOptionTerm of Constr.t
exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
type numnot_option =
  1. | Nop
  2. | Warning of Constrexpr.raw_natural_number
  3. | Abstract of Constrexpr.raw_natural_number
type int_ty = {
  1. uint : Names.inductive;
  2. int : Names.inductive;
}
type z_pos_ty = {
  1. z_ty : Names.inductive;
  2. pos_ty : Names.inductive;
}
type target_kind =
  1. | Int of int_ty
  2. | UInt of Names.inductive
  3. | Z of z_pos_ty
type option_kind =
  1. | Option
  2. | Direct
type conversion_kind = target_kind * option_kind
type numeral_notation_obj = {
  1. to_kind : conversion_kind;
  2. to_ty : Names.GlobRef.t;
  3. of_kind : conversion_kind;
  4. of_ty : Names.GlobRef.t;
  5. num_ty : Libnames.qualid;
  6. warning : numnot_option;
}
type prim_token_interp_info =
  1. | Uid of prim_token_uid
  2. | NumeralNotation of numeral_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 availability_of_prim_token : Constrexpr.prim_token -> Notation_term.scope_name -> Notation_term.subscopes -> delimiters option option
type interp_rule =
  1. | NotationRule of Notation_term.scope_name option * Constrexpr.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 -> unit
val declare_uninterpretation : interp_rule -> Notation_term.interpretation -> unit
type notation_rule = interp_rule * Notation_term.interpretation * int option
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 : (Notation_term.scope_name option * Constrexpr.notation) -> Notation_term.subscopes -> (Notation_term.scope_name option * delimiters option) option
val interp_notation_as_global_reference : ?loc:Loc.t -> (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 : 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 : Evd.evar_map -> EConstr.types -> Notation_term.scope_name option list
val compute_type_scope : 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 : Classops.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 decompose_notation_key : Constrexpr.notation -> Constrexpr.notation_entry_level * 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
type entry_coercion = Constrexpr.notation list
val declare_entry_coercion : Constrexpr.notation -> 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 with_notation_protection : ('a -> 'b) -> 'a -> 'b
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