aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/README.md1
-rw-r--r--dev/doc/changes.md10
2 files changed, 10 insertions, 1 deletions
diff --git a/dev/doc/README.md b/dev/doc/README.md
index 223cf6286e..c764455aed 100644
--- a/dev/doc/README.md
+++ b/dev/doc/README.md
@@ -16,7 +16,6 @@ $ opam init --comp <latest-ocaml-version>
~/.bashrc and ~/.ocamlinit files.
$ source ~/.bashrc
-$ opam install camlp5
# needed if you want to build "coqide" target
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 30a2967259..acb0d80c18 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,15 @@
## Changes between Coq 8.9 and Coq 8.10
+### ML4 Pre Processing
+
+- Support for `.ml4` files, processed by camlp5 has been removed in
+ favor of `.mlg` files processed by `coqpp`.
+
+ Porting is usually straightforward, and involves renaming the
+ `file.ml4` file to `file.mlg` and adding a few brackets.
+
+ See "Transitioning away from Camlp5" below for update instructions.
+
### ML API
General deprecation