From cc1212c3cfbd9c39cbe981210758c67cf9095be2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 27 Apr 2017 17:25:14 +0200 Subject: Tentative note in CHANGES about now applying βι while typing "match" branches. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- CHANGES | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 60b88ea8d..8cb5573b2 100644 --- a/CHANGES +++ b/CHANGES @@ -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 -- cgit v1.2.3