aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-08-01 17:20:55 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-08-03 23:31:08 +0200
commit5de89439d459edd402328a1e437be4d8cd2e4f46 (patch)
treef473c0f26b211c1ca31259e3fd85acf12ff42769 /printing
parent6dde48d3a75f3b8ffc960c4ac3f668ff93e93297 (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