From 62c141be71dd3c542824c19429eac0fdd686c9cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 18:39:15 +0100
Subject: Optimizing the computation of frozen evars.

---
 pretyping/unification.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f97f6fbc57..6cb1bc7028 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1450,9 +1450,7 @@ let default_matching_core_flags sigma =
   check_applied_meta_types = true;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = false;
-  frozen_evars =
-    fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
-      sigma Evar.Set.empty;
+  frozen_evars = Evar.Map.domain (Evd.undefined_map sigma);
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
   modulo_eta = false;
-- 
cgit v1.2.3