diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-01 17:20:55 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-03 23:31:08 +0200 |
| commit | 5de89439d459edd402328a1e437be4d8cd2e4f46 (patch) | |
| tree | f473c0f26b211c1ca31259e3fd85acf12ff42769 /library/global.ml | |
| parent | 6dde48d3a75f3b8ffc960c4ac3f668ff93e93297 (diff) | |
- Fix has_undefined_evars not using its or_sorts argument anymore.
- Allow apply's unification to use conversion even if some polymorphic
constants appear in the goal (consistent with occur_meta_or_evar, and
evarconv in general).
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions