From bcb425ead1d12d6e800f9f13f28b34da529c463e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Thu, 7 Aug 2014 14:08:29 +0200
Subject: Bettre pretty-printing of evar maps, avoids printing universe
 information for typeclass errors.

---
 toplevel/himsg.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 7497393e5..4e3d460de 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -875,7 +875,7 @@ let pr_constraints printenv env evd evars cstrs =
       pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs)
     else
       let filter evk _ = Evar.Map.mem evk evars in
-      pr_evar_map_filter filter evd
+      pr_evar_map_filter ~with_univs:false filter evd
 
 let explain_unsatisfiable_constraints env evd constr comp =
   let (_, constraints) = Evd.extract_all_conv_pbs evd in
-- 
cgit v1.2.3