diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-20 10:14:36 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-20 10:14:36 +0100 |
| commit | 6ef1e22f17b7a4d16fbc519240b4df1e3915ffef (patch) | |
| tree | 959866971140bfd88f479a3d6cd1d6dcdde04b9d /library/univops.ml | |
| parent | edf1a8f36f75861b822081b3825357e122b6937d (diff) | |
| parent | 900ead851016c9056fd61a772b38602576f4986c (diff) | |
Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces unbound rel
Diffstat (limited to 'library/univops.ml')
0 files changed, 0 insertions, 0 deletions