aboutsummaryrefslogtreecommitdiff
path: root/API/API.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-11-20 10:14:36 +0100
committerMaxime Dénès2017-11-20 10:14:36 +0100
commit6ef1e22f17b7a4d16fbc519240b4df1e3915ffef (patch)
tree959866971140bfd88f479a3d6cd1d6dcdde04b9d /API/API.ml
parentedf1a8f36f75861b822081b3825357e122b6937d (diff)
parent900ead851016c9056fd61a772b38602576f4986c (diff)
Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces unbound rel
Diffstat (limited to 'API/API.ml')
0 files changed, 0 insertions, 0 deletions