package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception CannotCoerceTo of string
module Value : sig ... end
val coerce_to_constr_context : Value.t -> EConstr.constr
val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t
val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Names.Id.t
val coerce_to_intro_pattern_naming : Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
val coerce_to_hint_base : Value.t -> string
val coerce_to_int : Value.t -> int
val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr
val coerce_to_closed_constr : Environ.env -> Value.t -> EConstr.constr
val coerce_to_evaluable_ref : Environ.env -> Evd.evar_map -> Value.t -> Names.evaluable_global_reference
val coerce_to_constr_list : Environ.env -> Value.t -> EConstr.constr list
val coerce_to_intro_pattern_list : ?loc:Loc.t -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t
val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t list
val coerce_to_reference : Evd.evar_map -> Value.t -> Names.GlobRef.t
val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> Tactypes.quantified_hypothesis
val coerce_to_decl_or_quant_hyp : Evd.evar_map -> Value.t -> Tactypes.quantified_hypothesis
val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list
val error_ltac_variable : ?loc:Loc.t -> Names.Id.t -> (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a
type appl =
  1. | UnnamedAppl
  2. | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list
val pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.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