diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-07-17 22:33:53 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-07-18 16:14:39 +0200 |
| commit | 1517d56d3588eaa9097683bc56c987069f04592f (patch) | |
| tree | 0cfe493b1cc294f2c467b4db5a0e5e8e7cd55dbc /library/nameops.ml | |
| parent | 0315a5d93c2de996f5c91bd2af827d3984ec1ad8 (diff) | |
Improve do_split option of typeclass resolution
It used to compute the dependencies of all undefined evars of the
evar_map, while only the dependencies of resolvable evars are necessary.
Diffstat (limited to 'library/nameops.ml')
0 files changed, 0 insertions, 0 deletions