aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2016-11-16 11:17:39 +0100
committerEmilio Jesus Gallego Arias2016-11-16 11:17:39 +0100
commit1053c873bdaedf37c1fd35be4e7021bfc806c23d (patch)
treea44ba5953df5acc17b710e20426db115521de111
parent3a51aa7265f35dd3cbf3f7bff858d663e4406146 (diff)
[doc] Mention XML protocol on changes.
It may be worth it, also added a note about file reorganization.
-rw-r--r--CHANGES5
-rw-r--r--dev/doc/changes.txt2
2 files changed, 7 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index c08d782b75..984e91946b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -104,6 +104,7 @@ Notations
- "Bind Scope" can once again bind "Funclass" and "Sortclass".
General infrastructure
+
- New configurable warning system which can be controlled with the vernacular
command "Set Warnings", or, under coqc/coqtop, with the flag "-w". In
particular, the default is now that warnings are printed by coqc.
@@ -122,6 +123,10 @@ Tools
Verbose Compat vernacular, since these warnings can now be silenced or
turned into errors using "-w".
+XML protocol
+
+- message format has changed, see dev/doc/changes.txt for more details.
+
Many bug fixes, minor changes and documentation improvements are not mentioned
here.
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 79a0c6312a..d052468f99 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -14,6 +14,8 @@ kernel/closure.ml{,i} -> kernel/cClosure.ml{,i}
lib/errors.ml{,i} -> lib/cErrors.ml{,i}
toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i}
+All IDE-specific files, including the XML protocol have been moved to ide/
+
** Reduction functions **
In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX,