Merge PR #13379: Add a new evar source to refer to evars which are types of evars

Reviewed-by: SkySkimmer

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