diff options
| -rw-r--r-- | CHANGES | 10 |
1 files changed, 10 insertions, 0 deletions
@@ -6,6 +6,16 @@ Tactics - New tactic "ClearBody H" to clear the body of definitions in local context - New tactic "Assert H := c" for forward reasoning +Efficiency + +- Improved efficiency wrt .vo sizes and compilation times + +Bugs + +- Apply "universe anomaly" bug fixed +- Bug with recursive inductive types involving let-in fixed +- Confusion between implicit args of locals and globals of same base name fixed +- NatRing works (to check) ---------------------------------------------------------------------------- Changes from V6.3.1 and V7.0 to V7.1 |