diff options
| author | Hugo Herbelin | 2020-05-10 21:48:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-13 12:13:15 +0200 |
| commit | 1e80f730590ba309b6eb1ae26832984fa7357761 (patch) | |
| tree | b663c20078deaef47dfb57ff7c112f321581163a /dev/base_include | |
| parent | 67f0e9fd40dc2f7b30a8aec4c7efb032e61a001e (diff) | |
Fixes #12233 (wrong printing env in presence of match branches eta-expansion).
At the same time, we propagate the correct binder relevance in detyping.
Note that this would be fixed by enforcing the context of branches in
the syntax of "Case".
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions