From 9f65b8bf9775dd571a806e10ac356b1b8f8ae2c5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 8 Oct 2018 02:14:07 +0200
Subject: Cleanup evar_extra: remove evar_info's store and add maps to evar_map

---
 engine/termops.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index e1f5fb0d7f..c4b57e4dd2 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -365,12 +365,18 @@ let pr_evar_map_gen with_univs pr_evars sigma =
     else
     str "CONSTRAINTS:" ++ brk (0, 1) ++
       pr_evar_constraints sigma conv_pbs ++ fnl ()
+  and unresolvables =
+    let evars = Evd.unresolvable_evars sigma in
+    if Evar.Set.is_empty evars then mt ()
+    else
+      str "UNRESOLVABLE:" ++ brk (0, 1) ++
+      prlist_with_sep spc (pr_existential_key sigma) (Evar.Set.elements evars) ++ fnl ()
   and metas =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
       str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
   in
-  evs ++ svs ++ cstrs ++ metas
+  evs ++ svs ++ cstrs ++ unresolvables ++ metas
 
 let pr_evar_list sigma l =
   let open Evd in
-- 
cgit v1.2.3