Module `Ltac_plugin.Taccoerce`Source

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.

Sourcetype appl =

| UnnamedAppl
(*
For generic applications: nothing is printed
*)
| 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

Sourcetype tacvalue =

| VFun of appl * Tacexpr.ltac_trace * Loc.t option * Geninterp.Val.t Names.Id.Map.t * Names.Name.t list * Tacexpr.glob_tactic_expr
| VRec of Geninterp.Val.t Names.Id.Map.t Stdlib.ref * Tacexpr.glob_tactic_expr

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

Source

val 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

Source

val coerce_to_intro_pattern : 
  Evd.evar_map ->
  Value.t ->
  Tactypes.delayed_open_constr Tactypes.intro_pattern_expr

Source

val 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

Source

val coerce_to_constr : 
  Environ.env ->
  Value.t ->
  Ltac_pretype.constr_under_binders

Sourceval coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr

Sourceval coerce_to_closed_constr : Environ.env -> Value.t -> EConstr.constr

Source

val 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

Source

val 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

Source

val 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

Source

val coerce_to_quantified_hypothesis : 
  Evd.evar_map ->
  Value.t ->
  Tactypes.quantified_hypothesis

Source

val coerce_to_decl_or_quant_hyp : 
  Evd.evar_map ->
  Value.t ->
  Tactypes.quantified_hypothesis

Sourceval coerce_to_int_list : Value.t -> int list

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Taccoerce/index.html

Module `Ltac_plugin.Taccoerce`Source

High-level access to values

Coercion functions

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Taccoerce/index.html

Module Ltac_plugin.TaccoerceSource

High-level access to values

Coercion functions

Module `Ltac_plugin.Taccoerce`Source