diff options
| author | Matthieu Sozeau | 2018-08-15 17:29:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:16:28 +0100 |
| commit | acc4f5922dcc1f92f3dc3db653b7608949b60c2b (patch) | |
| tree | c2863e99b3fe9bd50391bf1159193e61d2826d75 /pretyping/evarsolve.mli | |
| parent | c002eae68ac12dc8ed92e906b346f73606e7fd69 (diff) | |
Add an helper [instantiate_evar] function
It does checking of evar instance and Evd.define, assuming an
occur-check has already been performed.
Diffstat (limited to 'pretyping/evarsolve.mli')
| -rw-r--r-- | pretyping/evarsolve.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 810796457f..dfadb4aaea 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -59,6 +59,17 @@ type unifier = unify_flags -> unification_kind -> type conversion_check = unify_flags -> unification_kind -> env -> evar_map -> conv_pb -> constr -> constr -> bool +(** [instantiate_evar unify flags env sigma ev c] defines the evar [ev] with [c], + checking that the type of [c] is unifiable with [ev]'s declared type first. + + Preconditions: + - [ev] does not occur in [c]. + - [c] does not contain any Meta(_) + *) + +val instantiate_evar : unifier -> unify_flags -> evar_map -> + Evar.t -> constr -> evar_map + (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is @@ -67,6 +78,7 @@ type conversion_check = unify_flags -> unification_kind -> val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map + val refresh_universes : ?status:Evd.rigid -> ?onlyalg:bool (* Only algebraic universes *) -> |