Add a new evar source to refer to evars which are types of evars.

To tie the knot (since the evar depends on the evar type and the
source of the evar type of the evar), we use an "update_source"
function.

An alternative could be to provide a function to build both an evar
with its evar type directly in evd.ml...

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 *)