diff options
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 14 |
1 files changed, 13 insertions, 1 deletions
@@ -17,7 +17,19 @@ Tactics Most notably, the new implementation recognizes Miller patterns that were missed before because of a missing normalization step. Hopefully this should be fairly uncommon. -- "auto with real" can now discharge comparisons of literals +- Tactic "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. + +Vernacular Commands + +- Goals context can be printed in a more compact way when "Set + Printing Compact Contexts" is activated. + +- The deprecated `Save` vernacular and its form `Save Theorem id` to + close proofs have been removed from the syntax. Please use `Qed`. Standard Library |