diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-15 16:43:42 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-15 16:43:42 +0000 |
| commit | d536aeb0c465b62c708ba4c70fd31b82c24168a5 (patch) | |
| tree | d064289b76beb81b29f3173df6670d0a93847de5 /pretyping/evd.mli | |
| parent | ed39b35b780c1fac9eb110f303014683e6640c01 (diff) | |
Misc improvements about evar_map
- A Evd.defined_evars to keep only this part of the evar_map
- One Evd.fold less in Typeclasses.mark_unresolvables
- We check that only undefined evar_map could be set unresolvable
- A duplicated function in himsg.ml
TODO: some calls to Evd.fold(_undefined) would be faster if written
as Map.map or Map.mapi.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13716 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 90da5d389..751009434 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -182,6 +182,7 @@ val evars_reset_evd : evar_map -> evar_map -> evar_map for moving to evarutils *) val is_undefined_evar : evar_map -> constr -> bool val undefined_evars : evar_map -> evar_map +val defined_evars : evar_map -> evar_map (* [fold_undefined f m] iterates ("folds") function [f] over the undefined evars (that is, whose value is [Evar_empty]) of map [m]. It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *) |