diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-26 16:00:09 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-15 13:36:10 +0100 |
| commit | 900ead851016c9056fd61a772b38602576f4986c (patch) | |
| tree | 6af32625267038477f58456c1bf9a7b74aaf26a8 /library/univops.ml | |
| parent | a2b02cb9142984b912bf01cea09449d767326f19 (diff) | |
Fix #5761: cbv on undefined evars under binders produces unbound rel
When an evar is undefined we need to substitute inside the evar instance.
With help from @herbelin and @psteckler to identify the issue from a
large test case.
Diffstat (limited to 'library/univops.ml')
0 files changed, 0 insertions, 0 deletions