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, 7 insertions, 0 deletions

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9d86ea90e6..777b3b0c96 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -572,6 +572,13 @@ let rec explain_evar_kind env sigma evk ty =
       strbrk "the type of " ++ Id.print id
   | Evar_kinds.BinderType Anonymous ->
       strbrk "the type of this 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 -> strbrk "an internal placeholder" in
+      strbrk "the type of " ++ pp
   | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
       let id = Option.get ido in
       strbrk "the implicit parameter " ++ Id.print id ++ spc () ++ str "of" ++