aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CHANGES3
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 577a828f3d..2e828267db 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,9 @@ Changes from V8.1beta to V8.1
- [rewrite ... in H] now fails if [H] is used either in an hypothesis
or in the goal.
- The semantics of [rewrite ... in *] has been slightly modified (see doc).
+- Support for "as" clause in tactic injection
+- Fix for notations involving basic "match" expressions
+- Numerous reported bugs solved (some of them leading to incompatibilities)
Changes from V8.0 to V8.1beta