diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-20 11:39:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-20 11:39:59 +0200 |
| commit | dbe1c641164fc797edf0420f5f5a5e8b60b5a05a (patch) | |
| tree | f0f4e297a03720e7b60bcc4c4a13eb1deecfe6f1 /pretyping/pretyping.ml | |
| parent | a91d15dcb4c691463f0ad6f0e7277a52464d897c (diff) | |
| parent | 088b3161c93e46ec2d865fe71a206cee15acd30c (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'pretyping/pretyping.ml')
| -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 5d1f77a5a..efc42aab7 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)) |