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 /printing | |
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 'printing')
0 files changed, 0 insertions, 0 deletions