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

Reviewed-by: SkySkimmer

1 files changed, 7 insertions, 0 deletions

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