aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.md5
-rw-r--r--dev/doc/xml-protocol.md4
2 files changed, 7 insertions, 2 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6d5023405a..1eea2443fe 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -88,6 +88,11 @@ Primitive number parsers
have been split over three files (plugins/syntax/positive_syntax.ml,
plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml).
+Parsing
+
+- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules
+ Pcoq.Entry and Pcoq.Parsable were introduced to replace it.
+
### Unit testing
The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index b35571e9ca..48671c03b6 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -10,9 +10,9 @@ versions of Proof General.
A somewhat out-of-date description of the async state machine is
[documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md).
-OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli).
+OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml).
-Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt).
+Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md).
* [Commands](#commands)
- [About](#command-about)