diff options
| author | Pierre-Marie Pédrot | 2016-02-03 18:39:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-03 20:24:06 +0100 |
| commit | 62c141be71dd3c542824c19429eac0fdd686c9cb (patch) | |
| tree | be06b8dd5a8326bfbb07ea52a14208d71a509f13 | |
| parent | 0ee0b7d2f2365da6e63bc2e94d66f9c5fe1ebe6a (diff) | |
Optimizing the computation of frozen evars.
| -rw-r--r-- | pretyping/unification.ml | 4 |
1 files changed, 1 insertions, 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; |