GlobEnv (rocq-runtime.GlobEnv)

type t

To embed constr in glob_constr

type 'a obj_interp_fun =
  ?loc:Loc.t ->
  poly:PolyFlags.t ->
  t ->
  Evd.evar_map ->
  Evardefine.type_constraint ->
  'a ->
  EConstr.unsafe_judgment * Evd.evar_map

val register_constr_interp0 : 
  (_, 'g) GenConstr.tag ->
  '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

val make : Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> t

Export the underlying environment

val env : t -> Environ.env

val renamed_env : t -> Environ.env

val lfun : t -> Ltac_pretype.unbound_ltac_var_map

val vars_of_env : t -> Names.Id.Set.t

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

val push_rel : 
  Evd.evar_map ->
  EConstr.rel_declaration ->
  t ->
  EConstr.rel_declaration * t

val push_rel_context : 
  ?force_names:bool ->
  Evd.evar_map ->
  EConstr.rel_context ->
  t ->
  EConstr.rel_context * t

val push_rec_types : 
  Evd.evar_map ->
  (Names.Name.t EConstr.binder_annot array * EConstr.constr array) ->
  t ->
  Names.Name.t EConstr.binder_annot array * t

Declare an evar using renaming information

val new_evar : 
  t ->
  Evd.evar_map ->
  ?src:Evar_kinds.t Loc.located ->
  ?rrpat:bool ->
  ?naming:Namegen.intro_pattern_naming_expr ->
  ?relevance:EConstr.ERelevance.t ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

val new_type_evar : 
  t ->
  Evd.evar_map ->
  src:Evar_kinds.t Loc.located ->
  Evd.evar_map * EConstr.constr

val 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.

val 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

val interp_ltac_variable : 
  ?loc:Loc.t ->
  (t -> Glob_term.glob_constr -> Evd.evar_map * EConstr.unsafe_judgment) ->
  t ->
  Evd.evar_map ->
  Names.Id.t ->
  Evd.evar_map * EConstr.unsafe_judgment

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

val interp_glob_genarg : 
  ?loc:Loc.t ->
  poly:PolyFlags.t ->
  t ->
  Evd.evar_map ->
  Evardefine.type_constraint ->
  GenConstr.glb ->
  EConstr.unsafe_judgment * Evd.evar_map