diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-27 17:25:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-27 17:27:33 +0200 |
| commit | cc1212c3cfbd9c39cbe981210758c67cf9095be2 (patch) | |
| tree | e53a09690c6e9dd056c0cd405d3e15a055307966 /pretyping/locusops.ml | |
| parent | 9839375100365ea3bd28bfc2efdb701db7d83adb (diff) | |
Tentative note in CHANGES about now applying βι while typing "match" branches.
In practice, this is almost invisible except when using "refine". So,
in some sense, it is aligning the behavior of pretyping on the one of
logic.ml's "refine" so that the more natural behavior of 8.4's refine
on this issue is restored.
Diffstat (limited to 'pretyping/locusops.ml')
0 files changed, 0 insertions, 0 deletions