diff options
| author | Pierre-Marie Pédrot | 2016-05-12 18:10:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-12 19:00:54 +0200 |
| commit | 123504209e35b98ac14956ec6950cb7cd8b0089b (patch) | |
| tree | ae2e3b31a7fa0dcded2862d18a486bee0c984d40 | |
| parent | c5de2c3a2aa96c468e7583577141a93e359a9baf (diff) | |
Small optimization in evar resolution.
Instead of rebuilding a whole set of evars just to make a typeclass filter,
we use the source evarmap.
| -rw-r--r-- | pretyping/pretyping.ml | 5 |
1 files 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)) |