package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return something sensible according to the object content.

exception CannotCoerceTo of string

Exception raised whenever a coercion failed.

High-level access to values

The of_* functions cast a given argument into a value. The to_* do the converse, and return None if there is a type mismatch.

module Value : sig ... end
Coercion functions
val coerce_to_constr_context : Value.t -> Constr_matching.context
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 -> Tacred.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
Missing generic arguments
val error_ltac_variable : ?loc:Loc.t -> Names.Id.t -> (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a
type appl =
  1. | UnnamedAppl
    (*

    For generic applications: nothing is printed

    *)
  2. | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list
    (*

    For calls to global constants, some may alias other.

    *)

Abstract application, to print ltac functions

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