package coq

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

Type of environment extended with naming and ltac interpretation data

type t

To embed constr in glob_constr

type 'a obj_interp_fun = ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint -> 'a -> EConstr.unsafe_judgment * Evd.evar_map
val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> 'g obj_interp_fun -> unit
Pretyping name management

The following provides a level of abstraction for the kind of environment used for type inference (so-called pretyping); in particular:

  • it supports that term variables can be interpreted as Ltac variables pointing to the effective expected name
  • it incrementally and lazily computes the renaming of rel variables used to build purely-named evar contexts

Build a pretyping environment from an ltac environment

Export the underlying environment

val env : t -> Environ.env
val renamed_env : t -> Environ.env
val vars_of_env : t -> Names.Id.Set.t

Push to the environment, returning the declaration(s) with interpreted names

val push_rel_context : hypnaming:Evarutil.naming_mode -> ?force_names:bool -> Evd.evar_map -> EConstr.rel_context -> t -> EConstr.rel_context * t
val push_rec_types : hypnaming:Evarutil.naming_mode -> Evd.evar_map -> (Names.Name.t Context.binder_annot array * EConstr.constr array) -> t -> Names.Name.t Context.binder_annot array * t

Declare an evar using renaming information

hide_variable env na id tells to hide the binding of id in the ltac environment part of env and to additionally rebind it to id' in case na is some Name id'. It is useful e.g. for the dual status of y as term and binder. This is the case of match y return p with ... end which implicitly denotes match z as z return p with ... end when y is bound to a variable z and match t as y return p with ... end when y is bound to a non-variable term t. In the latter case, the binding of y to t should be hidden in p.

val hide_variable : t -> Names.Name.t -> Names.Id.t -> t

In case a variable is not bound by a term binder, look if it has an interpretation as a term in the ltac_var_map

Interp an identifier as an ltac variable bound to an identifier, or as the identifier itself if not bound to an ltac variable

val interp_ltac_id : t -> Names.Id.t -> Names.Id.t

Interpreting a generic argument, typically a "ltac:(...)", taking into account the possible renaming

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