diff options
| author | letouzey | 2010-12-15 16:43:42 +0000 |
|---|---|---|
| committer | letouzey | 2010-12-15 16:43:42 +0000 |
| commit | d536aeb0c465b62c708ba4c70fd31b82c24168a5 (patch) | |
| tree | d064289b76beb81b29f3173df6670d0a93847de5 /plugins/syntax/string_syntax.ml | |
| 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 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions