From 22a2cc1897f0d9f568ebfb807673e84f6ada491a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 27 Jan 2016 09:36:47 +0100
Subject: Fix bug #4537: Coq 8.5 is slower in typeclass resolution.

The performance enhancement introduced by a895b2c0 for non-polymorphic hints
was actually causing a huge regression in the polymorphic case (and was marked
as such). We fix this by only substituting the metas from the evarmap instead
of the whole evarmap.
---
 pretyping/evd.ml  | 4 ++++
 pretyping/evd.mli | 1 +
 2 files changed, 5 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 01083142b7..5441145189 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1467,6 +1467,10 @@ let map_metas_fvalue f evd =
   in
   set_metas evd (Metamap.smartmap map evd.metas)
 
+let map_metas f evd =
+  let map cl = map_clb f cl in
+  set_metas evd (Metamap.smartmap map evd.metas)
+
 let meta_opt_fvalue evd mv =
   match Metamap.find mv evd.metas with
     | Clval(_,b,_) -> Some b
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 0b4f185368..9cfca02ed8 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -455,6 +455,7 @@ val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map
 
 val undefined_metas : evar_map -> metavariable list
 val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map
+val map_metas : (constr -> constr) -> evar_map -> evar_map
 
 type metabinding = metavariable * constr * instance_status
 
-- 
cgit v1.2.3