aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-16 23:30:26 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-16 23:30:26 +0200
commit8c1d71db6b1eb95e67874417cc94f1d9728aff92 (patch)
treead11467c55b0d816d4d61ffcb42255afb9bc51c3
parent27b848dc388633ebfc58be8e7578069a3121dc27 (diff)
parent4078547a44619701e9a719876b716877d0368bc4 (diff)
Merge PR #7272: Mention other deprecations and fixes in CHANGES
-rw-r--r--CHANGES8
1 files changed, 7 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index 40e8547ae..502f848fb 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
===============================