(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
open Names open Environ open Evd open EConstr open Ltac_pretype open Evarutil
(** 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 -> unsafe_judgment * Evd.evar_map
val register_constr_interp0 :
('r, 'g, 't) Genarg.genarg_type -> 'g obj_interp_fun -> unit
(** {6 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 : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
(** Export the underlying environment *)
val env : t -> env val renamed_env : t -> env val lfun : t -> unbound_ltac_var_map
val vars_of_env : t -> Id.Set.t
(** Push to the environment, returning the declaration(s) with interpreted names *)
val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t EConstr.binder_annot array * constr array -> t -> Name.t EConstr.binder_annot array * t
(** Declare an evar using renaming information *)
val new_evar : t -> evar_map -> ?src:Evar_kinds.t Loc.located ->
?naming:Namegen.intro_pattern_naming_expr -> ?relevance:ERelevance.t ->
constr -> evar_map * constr
val new_type_evar : t -> evar_map -> src:Evar_kinds.t Loc.located -> evar_map * 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]. *) val lookup_renamed : t -> Id.t -> constr
(** [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 -> 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 *)
