diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-14 12:16:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-14 18:48:56 +0200 |
| commit | a895b2c0caf8ec9c0deb04b8dea890283bd7329d (patch) | |
| tree | 2894217b0404d4869e1421205851d2612196b7bb /dev | |
| parent | bf0499bc507d5a39c3d5e3bf1f69191339270729 (diff) | |
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.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f9f2e1b09..059c812ad 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) |