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.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/evd.mli')

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