aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CHANGES8
1 files changed, 7 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 40e8547ae9..502f848fb2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,7 +17,7 @@ Tactic language
- Support for fix/cofix added in Ltac "match" and "lazymatch".
-- Ltac backtraces now contain include trace information about tactics
+- Ltac backtraces now include trace information about tactics
called by OCaml-defined tactics.
Changes from 8.8+beta1 to 8.8.0
@@ -35,6 +35,12 @@ Tactic language
deprecated; please use `fix/cofix ident N` to explicitely name
hypothesis to be introduced.
+Documentation
+
+- The reference manual is now fully ported to Sphinx.
+
+Other small deprecations and bug fixes.
+
Changes from 8.7.2 to 8.8+beta1
===============================