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 /CHANGES | |
| 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 'CHANGES')
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -18,6 +18,11 @@ Tactics missed before because of a missing normalization step. Hopefully this should be fairly uncommon. - "auto with real" can now discharge comparisons of literals +- The types of variables in patterns of "match" are now + beta-iota-reduced after type-checking. This has an impact on the + type of the variables that the tactic "refine" introduces in the + context, producing types a priori closer to the expectations. + Standard Library |