package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

doc/coq-core.pretyping/GlobEnv/index.html

Module GlobEnvSource

Type of environment extended with naming and ltac interpretation data

Sourcetype t

To embed constr in glob_constr

Sourcetype 'a obj_interp_fun = ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint -> 'a -> EConstr.unsafe_judgment * Evd.evar_map
Sourceval 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

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

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

Sourceval push_rel_context : hypnaming:Evarutil.naming_mode -> ?force_names:bool -> Evd.evar_map -> EConstr.rel_context -> t -> EConstr.rel_context * 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.

Sourceval 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

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

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