Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585(************************************************************************)(* * 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 CSigopen Namesopen Constropen Environ
type t = Evd.econstr(** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring that {!Constr.kind} does not observe defined evars. *)
(** {5 Universe variables} *)
module ERelevance :sig type t = Evd.erelevance (** Type of relevance marks up-to quality variable unification. *)
val make : Sorts.relevance -> t
val kind : Evd.evar_map -> t -> Sorts.relevance
val equal : Evd.evar_map -> t -> t -> bool
val relevant : t val irrelevant : t
val is_irrelevant : Evd.evar_map -> t -> boolend
module ESorts :sig type t = Evd.esorts (** Type of sorts up-to universe unification. Essentially a wrapper around Sorts.t so that normalization is ensured statically. *)
val make : Sorts.t -> t (** Turn a sort into an up-to sort. *)
val kind : Evd.evar_map -> t -> Sorts.t (** Returns the view into the current sort. Note that the kind of a variable may change if the unification state of the evar map changes. *)
val equal : Evd.evar_map -> t -> t -> bool
val is_prop : Evd.evar_map -> t -> bool val is_sprop : Evd.evar_map -> t -> bool val is_set : Evd.evar_map -> t -> bool
val prop : t val sprop : t val set : t val type1 : t
val super : Evd.evar_map -> t -> t
val relevance_of_sort : t -> ERelevance.t
val quality : Evd.evar_map -> t -> Sorts.Quality.t val quality_or_set : Evd.evar_map -> t -> UnivGen.QualityOrSet.tend
module EInstance :sig type t = Evd.einstance (** Type of universe instances up-to universe unification. Similar to [ESorts.t] for [UVars.Instance.t]. *)
val make : UVars.Instance.t -> t val kind : Evd.evar_map -> t -> UVars.Instance.t val equal : Evd.evar_map -> t -> t -> bool val empty : t val is_empty : t -> bool val length : t -> int * intend
type types = ttype constr = ttype existential = t pexistentialtype case_return = (t,ERelevance.t) pcase_returntype case_branch = (t,ERelevance.t) pcase_branchtype rec_declaration = (t, t, ERelevance.t) prec_declarationtype fixpoint = (t, t, ERelevance.t) pfixpointtype cofixpoint = (t, t, ERelevance.t) pcofixpointtype unsafe_judgment = (constr, types) Environ.punsafe_judgmenttype unsafe_type_judgment = (types, Evd.esorts) Environ.punsafe_type_judgmenttype named_declaration = (constr, types, ERelevance.t) Context.Named.Declaration.pttype rel_declaration = (constr, types, ERelevance.t) Context.Rel.Declaration.pttype named_context = (constr, types, ERelevance.t) Context.Named.pttype rel_context = (constr, types, ERelevance.t) Context.Rel.pttype 'a binder_annot = ('a,ERelevance.t) Context.pbinder_annot
val annotR : 'a -> 'a binder_annotval nameR : Id.t -> Name.t binder_annotval anonR : Name.t binder_annot
type case_invert = t pcase_inverttype case = (t, t, EInstance.t, ERelevance.t) pcase
type 'a puniverses = 'a * EInstance.t
(** {5 Destructors} *)
val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term(** Same as {!Constr.kind} except that it expands evars and normalizes universes on the fly. *)
val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, UVars.Instance.t, Sorts.relevance) Constr.kind_of_term
val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t(** Returns the evar-normal form of the argument. Note that this function is supposed to be called when the original term has not more free-evars anymore. If you need compatibility with the old semantics, set [abort_on_undefined_evars] to [false].
For getting the evar-normal form of a term with evars see {!Evarutil.nf_evar}. *)
val to_constr_opt : Evd.evar_map -> t -> Constr.t option(** Same as [to_constr], but returns [None] if some unresolved evars remain *)
type kind_of_type = | SortType of ESorts.t | CastType of types * t | ProdType of Name.t binder_annot * t * t | LetInType of Name.t binder_annot * t * t * t | AtomicType of t * t array
val kind_of_type : Evd.evar_map -> t -> kind_of_type
(** {5 Constructors} *)
val of_kind : (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term -> t(** Construct a term from a view. *)
val of_constr : Constr.t -> t(** Translate a kernel term into an incomplete term in O(1). *)
(** {5 Insensitive primitives}
Evar-insensitive versions of the corresponding functions. See the {!Constr} module for more information.
*)
(** {6 Constructors} *)
val mkRel : int -> tval mkVar : Id.t -> tval mkMeta : metavariable -> tval mkEvar : t pexistential -> tval mkSort : ESorts.t -> tval mkSProp : tval mkProp : tval mkSet : tval mkType : Univ.Universe.t -> tval mkCast : t * cast_kind * t -> tval mkProd : Name.t binder_annot * t * t -> tval mkLambda : Name.t binder_annot * t * t -> tval mkLetIn : Name.t binder_annot * t * t * t -> tval mkApp : t * t array -> tval mkConstU : Constant.t * EInstance.t -> tval mkProj : (Projection.t * ERelevance.t * t) -> tval mkIndU : inductive * EInstance.t -> tval mkConstructU : constructor * EInstance.t -> tval mkConstructUi : (inductive * EInstance.t) * int -> tval mkCase : case -> tval mkFix : (t, t, ERelevance.t) pfixpoint -> tval mkCoFix : (t, t, ERelevance.t) pcofixpoint -> tval mkArrow : t -> ERelevance.t -> t -> tval mkArrowR : t -> t -> tval mkInt : Uint63.t -> tval mkFloat : Float64.t -> tval mkString : Pstring.t -> tval mkArray : EInstance.t * t array * t * t -> t
module UnsafeMonomorphic : sig val mkConst : Constant.t -> t val mkInd : inductive -> t val mkConstruct : constructor -> tend
val mkRef : GlobRef.t * EInstance.t -> t
val type1 : t
val applist : t * t list -> tval applistc : t -> t list -> t
(** { Abstracting/generalizing over binders } *)
(** it = iterated or_LetIn = turn a local definition into a LetIn wo_LetIn = inlines local definitions (i.e. substitute them in the body) Named = binding is by name and the combinators turn it into a binding by index (complexity is nb(binders) * size(term)) *)
val it_mkProd : t -> (Name.t binder_annot * t) list -> tval it_mkLambda : t -> (Name.t binder_annot * t) list -> t
val mkProd_or_LetIn : rel_declaration -> t -> tval mkLambda_or_LetIn : rel_declaration -> t -> tval it_mkProd_or_LetIn : t -> rel_context -> tval it_mkLambda_or_LetIn : t -> rel_context -> t
val mkProd_wo_LetIn : rel_declaration -> t -> tval mkLambda_wo_LetIn : rel_declaration -> t -> tval it_mkProd_wo_LetIn : t -> rel_context -> tval it_mkLambda_wo_LetIn : t -> rel_context -> t
val mkNamedProd : Evd.evar_map -> Id.t binder_annot -> types -> types -> typesval mkNamedLambda : Evd.evar_map -> Id.t binder_annot -> types -> constr -> constrval mkNamedLetIn : Evd.evar_map -> Id.t binder_annot -> constr -> types -> constr -> constr
val mkNamedProd_or_LetIn : Evd.evar_map -> named_declaration -> types -> typesval mkNamedLambda_or_LetIn : Evd.evar_map -> named_declaration -> types -> typesval it_mkNamedProd_or_LetIn : Evd.evar_map -> t -> named_context -> tval it_mkNamedLambda_or_LetIn : Evd.evar_map -> t -> named_context -> t
val mkNamedProd_wo_LetIn : Evd.evar_map -> named_declaration -> t -> tval it_mkNamedProd_wo_LetIn : Evd.evar_map -> t -> named_context -> t
val mkLEvar : Evd.evar_map -> Evar.t * t list -> t(** Variant of {!mkEvar} that removes identity variable instances from its argument. *)
(** {6 Simple case analysis} *)
val isRel : Evd.evar_map -> t -> boolval isVar : Evd.evar_map -> t -> boolval isInd : Evd.evar_map -> t -> boolval isRef : Evd.evar_map -> t -> boolval isEvar : Evd.evar_map -> t -> boolval isMeta : Evd.evar_map -> t -> boolval isSort : Evd.evar_map -> t -> boolval isCast : Evd.evar_map -> t -> boolval isApp : Evd.evar_map -> t -> boolval isLambda : Evd.evar_map -> t -> boolval isLetIn : Evd.evar_map -> t -> boolval isProd : Evd.evar_map -> t -> boolval isConst : Evd.evar_map -> t -> boolval isConstruct : Evd.evar_map -> t -> boolval isFix : Evd.evar_map -> t -> boolval isCoFix : Evd.evar_map -> t -> boolval isCase : Evd.evar_map -> t -> boolval isProj : Evd.evar_map -> t -> bool
val isType : Evd.evar_map -> constr -> bool
type arity = rel_context * ESorts.tval mkArity : arity -> typesval destArity : Evd.evar_map -> types -> arityval isArity : Evd.evar_map -> t -> bool
val isVarId : Evd.evar_map -> Id.t -> t -> boolval isRelN : Evd.evar_map -> int -> t -> boolval isRefX : Environ.env -> Evd.evar_map -> GlobRef.t -> t -> bool
(** The string is interpreted by [Rocqlib.lib_ref]. If it is not registered, return [false]. *)val is_lib_ref : Environ.env -> Evd.evar_map -> string -> t -> bool
val destRel : Evd.evar_map -> t -> intval destMeta : Evd.evar_map -> t -> metavariableval destVar : Evd.evar_map -> t -> Id.tval destSort : Evd.evar_map -> t -> ESorts.tval destCast : Evd.evar_map -> t -> t * cast_kind * tval destProd : Evd.evar_map -> t -> Name.t binder_annot * types * typesval destLambda : Evd.evar_map -> t -> Name.t binder_annot * types * tval destLetIn : Evd.evar_map -> t -> Name.t binder_annot * t * types * tval destApp : Evd.evar_map -> t -> t * t arrayval destConst : Evd.evar_map -> t -> Constant.t * EInstance.tval destEvar : Evd.evar_map -> t -> t pexistentialval destInd : Evd.evar_map -> t -> inductive * EInstance.tval destConstruct : Evd.evar_map -> t -> constructor * EInstance.tval destCase : Evd.evar_map -> t -> caseval destProj : Evd.evar_map -> t -> Projection.t * ERelevance.t * tval destFix : Evd.evar_map -> t -> (t, t, ERelevance.t) pfixpointval destCoFix : Evd.evar_map -> t -> (t, t, ERelevance.t) pcofixpoint
val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
val decompose_app : Evd.evar_map -> t -> t * t arrayval decompose_app_list : Evd.evar_map -> t -> t * t list
(** Pops lambda abstractions until there are no more, skipping casts. *)val decompose_lambda : Evd.evar_map -> t -> (Name.t binder_annot * t) list * t
(** Pops lambda abstractions and letins until there are no more, skipping casts. *)val decompose_lambda_decls : Evd.evar_map -> t -> rel_context * t
(** Pops [n] lambda abstractions, skipping casts.
@raise UserError if the term doesn't have enough lambdas. *)val decompose_lambda_n : Evd.evar_map -> int -> t -> (Name.t binder_annot * t) list * t
(** Pops [n] lambda abstractions, and pop letins only if needed to expose enough lambdas, skipping casts.
@raise UserError if the term doesn't have enough lambdas. *)val decompose_lambda_n_assum : Evd.evar_map -> int -> t -> rel_context * t
(** Pops [n] lambda abstractions and letins, skipping casts.
@raise UserError if the term doesn't have enough lambdas/letins. *)val decompose_lambda_n_decls : Evd.evar_map -> int -> t -> rel_context * t
(** Like [decompose_lambda_n_decls] but returns [None] instead of raising an anomaly when there are not enough abstractions. *)val decompose_lambda_n_decls_opt : Evd.evar_map -> int -> t -> (rel_context * t) option
val prod_decls : Evd.evar_map -> t -> rel_context
val to_lambda : Evd.evar_map -> int -> t -> t
val decompose_prod : Evd.evar_map -> t -> (Name.t binder_annot * t) list * tval decompose_prod_n : Evd.evar_map -> int -> t -> (Name.t binder_annot * t) list * tval decompose_prod_decls : Evd.evar_map -> t -> rel_context * tval decompose_prod_n_decls : Evd.evar_map -> int -> t -> rel_context * t
val existential_type : Evd.evar_map -> existential -> typesval whd_evar : Evd.evar_map -> constr -> constr
(** {6 Equality} *)
val eq_constr : Evd.evar_map -> t -> t -> boolval eq_constr_nounivs : Evd.evar_map -> t -> t -> boolval eq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option(** Does not produce QLeq nor QElimTo constraints *)
val leq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t optionval eq_existential : Evd.evar_map -> (t -> t -> bool) -> existential -> existential -> bool
(** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *)val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
(** {6 Iterators} *)
val map : Evd.evar_map -> (t -> t) -> t -> tval map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> tval map_branches : (t -> t) -> case_branch array -> case_branch arrayval map_return_predicate : (t -> t) -> case_return -> case_returnval map_existential : Evd.evar_map -> (t -> t) -> existential -> existentialval iter : Evd.evar_map -> (t -> unit) -> t -> unitval iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unitval iter_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unitval fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'aval fold_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> t -> 'b) -> 'a -> 'b -> t -> 'b
(** Gather the universes transitively used in the term, including in the type of evars appearing in it. *)val universes_of_constr : ?init:Sorts.Quality.Set.t * Univ.Level.Set.t -> Evd.evar_map -> t -> Sorts.Quality.Set.t * Univ.Level.Set.t
(** {6 Substitutions} *)
module Vars :sig
(** See vars.mli for the documentation of the functions below *)
type instance = t arraytype instance_list = t listtype substl = t list
val exliftn : Esubst.lift -> t -> tval lift : int -> t -> tval liftn : int -> int -> t -> tval substnl : substl -> int -> t -> tval substl : substl -> t -> tval subst1 : t -> t -> t
val substnl_decl : substl -> int -> rel_declaration -> rel_declarationval substl_decl : substl -> rel_declaration -> rel_declarationval subst1_decl : t -> rel_declaration -> rel_declaration
val replace_vars : Evd.evar_map -> (Id.t * t) list -> t -> tval substn_vars : Evd.evar_map -> int -> Id.t list -> t -> tval subst_vars : Evd.evar_map -> Id.t list -> t -> tval subst_var : Evd.evar_map -> Id.t -> t -> t
val noccurn : Evd.evar_map -> int -> t -> boolval noccur_between : Evd.evar_map -> int -> int -> t -> bool
val closedn : Evd.evar_map -> int -> t -> boolval closed0 : Evd.evar_map -> t -> bool
val subst_univs_level_constr : UVars.sort_level_subst -> t -> tval subst_instance_context : EInstance.t -> rel_context -> rel_contextval subst_instance_constr : EInstance.t -> t -> tval subst_instance_relevance : EInstance.t -> ERelevance.t -> ERelevance.t
val subst_of_rel_context_instance : rel_context -> instance -> substlval subst_of_rel_context_instance_list : rel_context -> instance_list -> substl
val liftn_rel_context : int -> int -> rel_context -> rel_contextval lift_rel_context : int -> rel_context -> rel_contextval substnl_rel_context : substl -> int -> rel_context -> rel_contextval substl_rel_context : substl -> rel_context -> rel_contextval smash_rel_context : rel_context -> rel_context
val esubst : (int -> 'a -> t) -> 'a Esubst.subs -> t -> t
type substituendval make_substituend : t -> substituendval lift_substituend : int -> substituend -> t
end
(** {5 Environment handling} *)
val push_rel : rel_declaration -> env -> envval push_rel_context : rel_context -> env -> envval push_rec_types : rec_declaration -> env -> env
val push_named : var_status -> named_declaration -> env -> envval push_named_context : (var_status * named_declaration) list -> env -> envval push_named_context_val : var_status -> named_declaration -> named_context_val -> named_context_val
val rel_context : env -> rel_contextval named_context : env -> named_context
val val_of_named_context : (var_status * named_declaration) list -> named_context_valval named_context_of_val : named_context_val -> named_contextval named_context_of_val_with_status : named_context_val -> (var_status * named_declaration) list
val fold_named_context_val : (named_context_val -> var_status -> named_declaration -> 'a -> 'a) -> named_context_val -> init:'a -> 'a
val fold_named_context : (env -> var_status -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
val lookup_rel : int -> env -> rel_declarationval lookup_named : variable -> env -> named_declarationval lookup_named_val : variable -> named_context_val -> named_declaration
(** [check_hyps_inclusion env gr hyps] Check that [hyps] are included in [env] and fails with error otherwise. *)val check_hyps_inclusion : env -> Names.GlobRef.t -> Constr.named_context -> unit
val lookup_constant : env -> Evd.evar_map -> Constant.t -> Declarations.constant_bodyval constant_value_in : env -> Evd.evar_map -> Constant.t * EInstance.t -> constr
val map_rel_context_in_env : (env -> constr -> constr) -> env -> rel_context -> rel_context
val match_named_context_val : named_context_val -> (var_status * named_declaration * named_context_val) option
(** [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] must preserve the name *)val map_named_val : (var_status -> named_declaration -> var_status * named_declaration) -> named_context_val -> named_context_val
val identity_subst_val : named_context_val -> t SList.t
(* XXX Missing Sigma proxy *)val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:EInstance.t -> Environ.env -> Evd.evar_map -> GlobRef.t -> Evd.evar_map * t
val expand_case : Environ.env -> Evd.evar_map -> case -> (t,t,ERelevance.t) Inductive.pexpanded_case
val annotate_case : Environ.env -> Evd.evar_map -> case -> case_info * EInstance.t * t array * ((rel_context * t) * ERelevance.t) * case_invert * t * (rel_context * t) array(** Same as above, but doesn't turn contexts into binders *)
val expand_branch : Environ.env -> Evd.evar_map -> EInstance.t -> t array -> constructor -> case_branch -> rel_context(** Given a universe instance and parameters for the inductive type, constructs the typed context in which the branch lives. *)
val contract_case : Environ.env -> Evd.evar_map -> (t,t,ERelevance.t) Inductive.pexpanded_case -> case
(** {5 Extra} *)
val of_existential : Constr.existential -> existentialval of_named_decl : Constr.named_declaration -> named_declarationval of_rel_decl : Constr.rel_declaration -> rel_declaration
val to_rel_decl : Evd.evar_map -> rel_declaration -> Constr.rel_declarationval to_named_decl : Evd.evar_map -> named_declaration -> Constr.named_declaration
val of_named_context : Constr.named_context -> named_contextval of_rel_context : Constr.rel_context -> rel_context
val to_named_context : Evd.evar_map -> named_context -> Constr.named_contextval to_rel_context : Evd.evar_map -> rel_context -> Constr.rel_context
val of_case_invert : Constr.case_invert -> case_invert
val of_constr_array : Constr.t array -> t array
val of_binder_annot : 'a Constr.binder_annot -> 'a binder_annot
val to_binder_annot : Evd.evar_map -> 'a binder_annot -> 'a Constr.binder_annot
(** {5 Unsafe operations} *)
module Unsafe :sig val to_constr : t -> Constr.t (** Physical identity. Does not care for defined evars. *)
val to_constr_array : t array -> Constr.t array (** Physical identity. Does not care for defined evars. *)
val to_binder_annot : 'a binder_annot -> 'a Constr.binder_annot
val to_rel_decl : (t, types, ERelevance.t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types, Sorts.relevance) Context.Rel.Declaration.pt (** Physical identity. Does not care for defined evars. *)
val to_named_decl : (t, types, ERelevance.t) Context.Named.Declaration.pt -> (Constr.t, Constr.types, Sorts.relevance) Context.Named.Declaration.pt (** Physical identity. Does not care for defined evars. *)
val to_named_context : (t, types, ERelevance.t) Context.Named.pt -> Constr.named_context
val to_rel_context : (t, types, ERelevance.t) Context.Rel.pt -> Constr.rel_context
val to_relevance : ERelevance.t -> Sorts.relevance
val to_sorts : ESorts.t -> Sorts.t (** Physical identity. Does not care for normalization. *)
val to_instance : EInstance.t -> UVars.Instance.t (** Physical identity. Does not care for normalization. *)
val to_case_invert : case_invert -> Constr.case_invert
val eq : (t, Constr.t) eq (** Use for transparent cast between types. *)
val relevance_eq : (ERelevance.t, Sorts.relevance) eqend
(** {5 Delayed evar expansion} *)
module Expand :sig
type t(** A variant of [EConstr.t] where evar substitution is performed on the fly. The [handle] type below is a kind of substitution that is needed to make sense of the delayed term. Such representation is more efficient than [EConstr.t] when iterating over a whole term.
Caveat: the [kind] function below only returns the expanded head of the term. This means that when it returns [Evar (evk, inst)], [evk] is guaranteed to be undefined in the evar map but [inst] is, in general, not the same as you would get after expansion. You must call [expand_instance] before performing any operation on it. *)
type kind = (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term
type handle
val make : Evd.econstr -> handle * tval repr : Evd.evar_map -> handle -> t -> Evd.econstrval liftn_handle : int -> handle -> handleval kind : Evd.evar_map -> handle -> t -> handle * kindval expand_instance : skip:bool -> Evd.undefined Evd.evar_info -> handle -> t SList.t -> t SList.tval iter : Evd.evar_map -> (handle -> t -> unit) -> handle -> kind -> unitval iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> handle -> t -> unit) -> 'a -> handle -> kind -> unit
end