diff options
| -rw-r--r-- | CHANGES | 32 |
1 files changed, 14 insertions, 18 deletions
@@ -1,6 +1,20 @@ Changes from V7.1 to V7.2 ======================== +Language + +- Automatic insertion of patterns for local definitions in the type of + the constructors of an inductive types (for compatibility with V6.3 + let-in style) +- Coercions allowed in Cases patterns + +Tactics + +- New tactic "ClearBody H" to clear the body of definitions in local context +- New tactic "Assert H := c" for forward reasoning +- Slight improvement in naming strategy for NewInduction/NewDestruct (may + occasionnally affect compatibility with V7.1 NewInduction/NewDestruct) + Standard library ---------------- @@ -18,24 +32,6 @@ Standard library - A new directory named [Sorting] contains a proof of a heapsort. (theory forgotten during the port of V6.3 to V7.0) - ----------------------------------------------------------------------------- -Changes from ??? to V7.1 -======================== - -Language - -- Automatic insertion of patterns for local definitions in the type of - the constructors of an inductive types (for compatibility with V6.3 - let-in style) - -Tactics - -- New tactic "ClearBody H" to clear the body of definitions in local context -- New tactic "Assert H := c" for forward reasoning -- Slight improvement in naming strategy for NewInduction/NewDestruct (may - occasionnally affect compatibility with V7.1 NewInduction/NewDestruct) - Efficiency - Improved efficiency wrt .vo sizes and compilation times |