Module Evarutil
Metas
val new_meta : unit -> Constr.metavariable
new_meta
is a generator of unique meta variables
val mk_new_meta : unit -> EConstr.constr
Creating a fresh evar given their type and context
val new_evar_from_context : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list -> ?naming:Namegen.intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> Environ.named_context_val -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.t
type naming_mode
=
|
KeepUserNameAndRenameExistingButSectionNames
|
KeepUserNameAndRenameExistingEvenSectionNames
|
KeepExistingNames
|
FailIfConflict
|
ProgramNaming
val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?abstract_arguments:Evd.Abstraction.t -> ?candidates:EConstr.constr list -> ?naming:Namegen.intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> ?hypnaming:naming_mode -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.t
val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?abstract_arguments:Evd.Abstraction.t -> ?candidates:EConstr.constr list -> ?naming:Namegen.intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> Environ.named_context_val -> Evd.evar_map -> EConstr.types -> Evd.evar_map * Evar.t
val new_pure_evar_full : Evd.evar_map -> ?typeclass_candidate:bool -> Evd.evar_info -> Evd.evar_map * Evar.t
val new_type_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?naming:Namegen.intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> Environ.env -> Evd.evar_map -> Evd.rigid -> Evd.evar_map * (EConstr.constr * Sorts.t)
Create a new Type existential variable, as we keep track of them during type-checking and unification.
val new_Type : ?rigid:Evd.rigid -> Evd.evar_map -> Evd.evar_map * EConstr.constr
val new_global : Evd.evar_map -> Names.GlobRef.t -> Evd.evar_map * EConstr.constr
val new_evar_instance : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?abstract_arguments:Evd.Abstraction.t -> ?candidates:EConstr.constr list -> ?naming:Namegen.intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> Environ.named_context_val -> Evd.evar_map -> EConstr.types -> EConstr.constr list -> Evd.evar_map * EConstr.constr
Create a fresh evar in a context different from its definition context:
new_evar_instance sign evd ty inst
creates a new evar of contextsign
and typety
,inst
is a mapping of the evar context to the context where the evar should occur. This means that the terms ofinst
are typed in the occurrence context and their type (seen as a telescope) issign
val make_pure_subst : Evd.evar_info -> 'a list -> (Names.Id.t * 'a) list
val safe_evar_value : Evd.evar_map -> Constr.existential -> Constr.constr option
Evars/Metas switching...
val non_instantiated : Evd.evar_map -> Evd.evar_info Evar.Map.t
Unification utils
val head_evar : Evd.evar_map -> EConstr.constr -> Evar.t
may raise NoHeadEvar
val whd_head_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val has_undefined_evars : Evd.evar_map -> EConstr.constr -> bool
val is_ground_term : Evd.evar_map -> EConstr.constr -> bool
val is_ground_env : Evd.evar_map -> Environ.env -> bool
val gather_dependent_evars : Evd.evar_map -> Evar.t list -> Evar.Set.t option Evar.Map.t
gather_dependent_evars evm seeds
classifies the evars inevm
as dependent_evars and goals (these may overlap). A goal is an evar inseeds
or an evar appearing in the (partial) definition of a goal. A dependent evar is an evar appearing in the type (hypotheses and conclusion) of a goal, or in the type or (partial) definition of a dependent evar. The value return is a map associating to each dependent evarNone
if it has no (partial) definition orSome s
ifs
is the list of evars appearing in its (partial) definition.
val advance : Evd.evar_map -> Evar.t -> Evar.t option
advance sigma g
returnsSome g'
ifg'
is undefined and is the current avatar ofg
(for instanceg
was changed byclear
intog'
). It returnsNone
ifg
has been (partially) solved.
val undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t
val undefined_evars_of_named_context : Evd.evar_map -> Constr.named_context -> Evar.Set.t
val undefined_evars_of_evar_info : Evd.evar_map -> Evd.evar_info -> Evar.Set.t
val create_undefined_evars_cache : unit -> undefined_evars_cache
val filtered_undefined_evars_of_evar_info : ?cache:undefined_evars_cache -> Evd.evar_map -> Evd.evar_info -> Evar.Set.t
val occur_evar_upto : Evd.evar_map -> Evar.t -> EConstr.constr -> bool
occur_evar_upto sigma k c
returnstrue
ifk
appears inc
. It looks up recursively insigma
for the value of existential variables.
Value/Type constraints
val judge_of_new_Type : Evd.evar_map -> Evd.evar_map * EConstr.unsafe_judgment
val whd_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val j_nf_evar : Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
val jl_nf_evar : Evd.evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list
val jv_nf_evar : Evd.evar_map -> EConstr.unsafe_judgment array -> EConstr.unsafe_judgment array
val tj_nf_evar : Evd.evar_map -> EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment
val nf_named_context_evar : Evd.evar_map -> Constr.named_context -> Constr.named_context
val nf_rel_context_evar : Evd.evar_map -> EConstr.rel_context -> EConstr.rel_context
val nf_env_evar : Evd.evar_map -> Environ.env -> Environ.env
val nf_evar_info : Evd.evar_map -> Evd.evar_info -> Evd.evar_info
val nf_evar_map : Evd.evar_map -> Evd.evar_map
val nf_evar_map_undefined : Evd.evar_map -> Evd.evar_map
val nf_evars_universes : Evd.evar_map -> Constr.constr -> Constr.constr
exception
Uninstantiated_evar of Evar.t
Replacing all evars, possibly raising
Uninstantiated_evar
val flush_and_check_evars : Evd.evar_map -> EConstr.constr -> Constr.constr
val finalize : ?abort_on_undefined_evars:bool -> Evd.evar_map -> ((EConstr.t -> Constr.t) -> 'a) -> Evd.evar_map * 'a
finalize env sigma f
combines universe minimisation, evar-and-universe normalisation and universe restriction.It minimizes universes in
sigma
, callsf
a normalisation function with respect to the updatedsigma
and restricts the local universes ofsigma
to those encountered while runningf
.Note that the normalizer passed to
f
holds some imperative state in its closure.
Term manipulation up to instantiation
val kind_of_term_upto : Evd.evar_map -> Constr.constr -> (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
Like
Constr.kind
except thatkind_of_term sigma t
exposest
as an evare
only ife
is uninstantiated insigma
. Otherwise the value ofe
insigma
is (recursively) used.
val eq_constr_univs_test : evd:Evd.evar_map -> extended_evd:Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
eq_constr_univs_test ~evd ~extended_evd t u
tests equality oft
andu
up to existential variable instantiation and equalisable universes. The termt
is interpreted inevd
whileu
is interpreted inextended_evd
. The universe constraints inextended_evd
are assumed to be an extension of those inevd
.
val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Evd.evar_map -> (Evd.evar_map, Univ.univ_inconsistency) Util.union
compare_cumulative_instances cv_pb variance u1 u2 sigma
ReturnsInl sigma'
wheresigma'
issigma
augmented with universe constraints such thatu1 cv_pb? u2
according tovariance
. Additionally flexible universes in irrelevant positions are unified if possible. ReturnsInr p
when the former is impossible.
val compare_constructor_instances : Evd.evar_map -> Univ.Instance.t -> Univ.Instance.t -> Evd.evar_map
We should only compare constructors at convertible types, so this is only an opportunity to unify universes.
type unification_pb
= Evd.conv_pb * Environ.env * EConstr.constr * EConstr.constr
Unification problems
val add_unification_pb : ?tail:bool -> unification_pb -> Evd.evar_map -> Evd.evar_map
add_unification_pb ?tail pb sigma
Add a unification problempb
tosigma
, if not already present. Put it at the end of the list iftail
is true, by default it is false.
Removing hyps in evars'context
raise OccurHypInSimpleClause if the removal breaks dependencies
type clear_dependency_error
=
|
OccurHypInSimpleClause of Names.Id.t option
|
EvarTypingBreak of Constr.existential
|
NoCandidatesLeft of Evar.t
exception
ClearDependencyError of Names.Id.t * clear_dependency_error * Names.GlobRef.t option
val restrict_evar : Evd.evar_map -> Evar.t -> Evd.Filter.t -> ?src:Evar_kinds.t Loc.located -> EConstr.constr list option -> Evd.evar_map * Evar.t
val clear_hyps_in_evi : Environ.env -> Evd.evar_map -> Environ.named_context_val -> EConstr.types -> Names.Id.Set.t -> Evd.evar_map * Environ.named_context_val * EConstr.types
val clear_hyps2_in_evi : Environ.env -> Evd.evar_map -> Environ.named_context_val -> EConstr.types -> EConstr.types -> Names.Id.Set.t -> Evd.evar_map * Environ.named_context_val * EConstr.types * EConstr.types
val empty_csubst : csubst
val csubst_subst : csubst -> EConstr.constr -> EConstr.constr
type ext_named_context
= csubst * Names.Id.Set.t * EConstr.named_context
val push_rel_decl_to_named_context : ?hypnaming:naming_mode -> Evd.evar_map -> EConstr.rel_declaration -> ext_named_context -> ext_named_context
val push_rel_context_to_named_context : ?hypnaming:naming_mode -> Environ.env -> Evd.evar_map -> EConstr.types -> Environ.named_context_val * EConstr.types * EConstr.constr list * csubst
val generalize_evar_over_rels : Evd.evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list
val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located
val meta_counter_summary_tag : int Summary.Dyn.tag