package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

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_evaluable_ref : Environ.env -> Evd.evar_map -> Value.t -> Evaluable.t
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_list : Value.t -> int list
Sourceval error_ltac_variable : ?loc:Loc.t -> Names.Id.t -> (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a
Sourceval pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t