From a895b2c0caf8ec9c0deb04b8dea890283bd7329d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Oct 2015 12:16:36 +0200
Subject: Fixing  perfomance issue of auto hints induced by universes.

Instead of brutally merging the whole evarmap coming from the clenv,
we remember the context associated to the hint and we only merge that tiny
part of constraints. We need to be careful for polymorphic hints though,
as we have to refresh them beforehand.
---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9f2e1b09e..059c812ad5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -165,7 +165,7 @@ let pp_state_t n = pp (Reductionops.pr_state n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
+let ppevm evd = pp(Evd.pr_evar_universe_context (Evd.evar_universe_context evd))
 let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
-- 
cgit v1.2.3