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...

5 files changed, 18 insertions, 0 deletions

diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 71d68f739e..fb41c4491e 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -40,6 +40,7 @@ type t =
   | ImplicitArg of GlobRef.t * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of Name.t
+  | EvarType of Id.t option * Evar.t (* type of an optionally named evar *)
   | NamedHole of Id.t (* coming from some ?[id] syntax *)
   | QuestionMark of question_mark
   | CasesType of bool (* true = a subterm of the type *)
diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli
index ffc57cfd15..b2b39d49be 100644
--- a/engine/evar_kinds.mli
+++ b/engine/evar_kinds.mli
@@ -39,6 +39,7 @@ type t =
   | ImplicitArg of GlobRef.t * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of Name.t
+  | EvarType of Id.t option * Evar.t (* type of an optionally named evar *)
   | NamedHole of Id.t (* coming from some ?[id] syntax *)
   | QuestionMark of question_mark
   | CasesType of bool (* true = a subterm of the type *)
diff --git a/engine/evd.ml b/engine/evd.ml
index 498a9d9825..59eea97ce9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1231,6 +1231,11 @@ let restrict evk filter ?candidates ?src evd =
   let evd = declare_future_goal evk' evd in
   (evd, evk')
 
+let update_source evd evk src =
+  let evar_info = EvMap.find evk evd.undf_evars in
+  let evar_info' = { evar_info with evar_source = src } in
+  { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars }
+
 (**********************************************************)
 (* Accessing metas *)
 
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 *)
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 693945d5ac..ccd49ca495 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -123,6 +123,13 @@ let pr_evar_source env sigma = function
       str "subterm of pattern-matching return predicate"
   | Evar_kinds.BinderType (Name id) -> str "type of " ++ Id.print id
   | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
+  | Evar_kinds.EvarType (ido,evk) ->
+      let pp = match ido with
+        | Some id -> str "?" ++ Id.print id
+        | None ->
+          try pr_existential_key sigma evk
+          with (* defined *) Not_found -> str "an internal placeholder" in
+     str "type of " ++ pp
   | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
       let open Globnames in
       let print_constr = print_kconstr in