package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

doc/ltac_plugin/Ltac_plugin/Taccoerce/index.html

Module Ltac_plugin.TaccoerceSource

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.

Sourceexception 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.

Sourcemodule Value : sig ... end
Coercion functions
Sourceval coerce_to_constr_context : Value.t -> Constr_matching.context
Sourceval coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t
Sourceval coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Names.Id.t
Sourceval coerce_to_intro_pattern_naming : Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
Sourceval coerce_to_hint_base : Value.t -> string
Sourceval coerce_to_int : Value.t -> int
Sourceval coerce_to_closed_constr : Environ.env -> Value.t -> EConstr.constr
Sourceval coerce_to_constr_list : Environ.env -> Value.t -> EConstr.constr list
Sourceval coerce_to_intro_pattern_list : ?loc:Loc.t -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
Sourceval coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t
Sourceval coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Names.Id.t list
Sourceval coerce_to_reference : Evd.evar_map -> Value.t -> Names.GlobRef.t
Sourceval coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> Tactypes.quantified_hypothesis
Sourceval coerce_to_decl_or_quant_hyp : Evd.evar_map -> Value.t -> Tactypes.quantified_hypothesis
Sourceval coerce_to_int_or_var_list : Value.t -> int Locus.or_var list
Missing generic arguments
Sourceval error_ltac_variable : ?loc:Loc.t -> Names.Id.t -> (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a
Sourcetype 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

Sourceval pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t