From e4f9b2a8af4489b9d7fb27dcd2f919a54491c402 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 5 Dec 2014 14:21:01 +0100
Subject: More consistent printing of evars in evar_map debugging printer.

---
 pretyping/evd.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9336841436..1d05d6c6e5 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -128,7 +128,7 @@ module Store = Store.Make(Dummy)
 
 type evar = Term.existential_key
 
-let string_of_existential evk = "?" ^ string_of_int (Evar.repr evk)
+let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
 
 type evar_body =
   | Evar_empty
@@ -1740,7 +1740,9 @@ let pr_evar_list sigma l =
   let pr (ev, evi) =
     h 0 (str (string_of_existential ev) ++
       str "==" ++ pr_evar_info evi ++
-      str " {" ++ pr_id (evar_ident ev sigma) ++ str "}")
+      (if evi.evar_body == Evar_empty
+       then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}"
+       else mt ()))
   in
   h 0 (prlist_with_sep fnl pr l)
 
-- 
cgit v1.2.3