diff options
| author | coqbot-app[bot] | 2020-11-26 10:13:28 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-26 10:13:28 +0000 |
| commit | 02a04a2a98cc20c83f8465ab992e39ce4380f94e (patch) | |
| tree | 3313d2fc661f2c778a89679a04c981b78d5860a5 /engine/evd.mli | |
| parent | bef0e543b812764db985f64421265637501f5f8d (diff) | |
| parent | 47910007a9eff37c9f364a269b46874165711abf (diff) | |
Merge PR #13379: Add a new evar source to refer to evars which are types of evars
Reviewed-by: SkySkimmer
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 1c5c65924c..911e00c23a 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -290,6 +290,10 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> possibly limiting the instances to a set of candidates (candidates are filtered according to the filter) *) +val update_source : evar_map -> Evar.t -> Evar_kinds.t located -> evar_map +(** To update the source a posteriori, e.g. when an evar type of + another evar has to refer to this other evar, with a mutual dependency *) + val get_aliased_evars : evar_map -> Evar.t Evar.Map.t (** The map of aliased evars *) |