From 123504209e35b98ac14956ec6950cb7cd8b0089b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 May 2016 18:10:34 +0200
Subject: Small optimization in evar resolution.

Instead of rebuilding a whole set of evars just to make a typeclass filter,
we use the source evarmap.
---
 pretyping/pretyping.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b33084a423..d6f8f0de5f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -184,8 +184,7 @@ type inference_flags = {
 }
 
 let frozen_holes (sigma, sigma') =
-  let fold evk _ accu = Evar.Set.add evk accu in
-  Evd.fold_undefined fold sigma Evar.Set.empty
+  (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma)
 
 let pending_holes (sigma, sigma') =
   let fold evk _ accu =
@@ -194,7 +193,7 @@ let pending_holes (sigma, sigma') =
   Evd.fold_undefined fold sigma' Evar.Set.empty
 
 let apply_typeclasses env evdref frozen fail_evar =
-  let filter_frozen evk = Evar.Set.mem evk frozen in
+  let filter_frozen = frozen in
   evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
 	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
-- 
cgit v1.2.3