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 (3)

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.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.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

Sourceval lookup_renamed : t -> Names.Id.t -> EConstr.constr

Lookup the ident in the context that would be used for an evar in this environment, producing a term (Var or Rel) valid in renamed_env.

hide_variable env id tells to hide the binding of id in the ltac environment part of env. 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.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