aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-11 01:33:53 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-11 01:33:53 +0200
commite372f0e5f0646eb4209baa06c874b4f041ed6574 (patch)
tree0eb3b9bc736d4e5cdcd022b315cf7c2a4f0731a0 /dev/doc
parentd47ddf56bc93ae16280ce8a845a4b004fef52fb8 (diff)
parenta9728d5a43e5c82fed9cac25e841107c4c95fc35 (diff)
Merge PR #7898: Remove camlp4 remains
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.md5
1 files changed, 5 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6d5023405..1eea2443f 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