6 files changed, 106 insertions, 10 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
new file mode 100644
index 0000000000..71fc396088
--- /dev/null
+++ b/dev/doc/MERGING.md
@@ -0,0 +1,78 @@
+# Merging changes in Coq
+
+This document describes how patches (submitted as Pull Requests) should be
+merged into the main repository (https://github.com/coq/coq).
+
+## Code owners
+
+The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
+system, two owners. One is the principal maintainer of the component, the other
+is the secondary maintainer.
+
+When a pull request is submitted, GitHub will automatically ask the principal
+maintainer for a review. If the pull request touches several parts, all the
+corresponding principal maintainers will be asked for a review.
+
+Maintainers are never assigned as reviewer on their own PRs.
+
+If a principal maintainer submits a PR that changes the component they own, they
+must assign the secondary maintainer as reviewer. They should also do it if they
+know they are not available to do the review.
+
+## Reviewing
+
+When maintainers receive a review request, they are expected to:
+
+* Put their name in the assignee field, if they are in charge of the component
+  that is the main target of the patch (or if they are the only maintainer asked
+  to review the PR).
+* Review the PR, approve it or request changes.
+* If they are the assignee, check if all reviewers approved the PR. If not,
+  regularly ping the author (if changes should be implemented) or the reviewers
+  (if reviews are missing). The assignee ensures that any requests for more
+  discussion have been granted. When the discussion has converged and ALL
+  REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging
+  process described below.
+
+In all cases, maintainers can delegate reviews to the other maintainer of the
+same component, except if it would lead to a maintainer reviewing their own
+patch.
+
+A maintainer is expected to be reasonably reactive, but no specific timeframe is
+given for reviewing.
+
+(*) In case a component is touched in a trivial way (adding/removing one file in
+a `Makefile`, etc), or by applying a systematic process (global renaming,
+deprecationg propagation, etc) that has been reviewed globally, the assignee can
+say in a comment they think a review is not required and proceed with the merge.
+
+## Merging
+
+Once all reviewers approved the PR, the assignee is expected to check that CI
+completed without relevant failures, and that the PR comes with appropriate
+documentation and test cases. If not, they should leave a comment on the PR and
+put the approriate label. Otherwise, they are expected to merge the PR using the
+[merge script](/dev/tools/merge-pr.sh).
+
+When the PR has conflicts, the assignee can either:
+- ask the author to rebase the branch, fixing the conflicts
+- warn the author that they are going to rebase the branch, and push to the
+  branch directly
+
+In both cases, CI should be run again.
+
+In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix
+the conflicts in the merge commit (following the same steps as below), and push
+to `master` directly. Don't use the GitHub interface to fix these conflicts.
+
+The command to be used is:
+```
+$ dev/tools/merge-pr XXXX
+```
+where `XXXX` is the number of the PR to be merged. This operation should be followed by a push.
+
+Maintainers MUST NOT merge their own patches.
+
+DON'T USE the GitHub interface for merging, since it will prevent the automated
+backport script from operating properly, generates bad commit messages, and a
+messy history when there are conflicts.
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index f3fc13e969..abba13428f 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -46,7 +46,7 @@ see build-system.txt .
 .ml4 files
 ----------
 
-.ml4 are converted to .ml by camlp4. By default, they are produced
+.ml4 are converted to .ml by camlp5. By default, they are produced
 in the binary ast format understood by ocamlc/ocamlopt/ocamldep.
 Pros:
  - faster than parsing clear-text source file.
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 873adc1b22..fd3101613a 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -88,7 +88,7 @@ bootstrapped. The dependencies of a file FOO are in FOO.d . This
 enables partial recalculation of dependencies (only the dependencies
 of changed files are recomputed).
 
-If you add a dependency to a Coq camlp4 extension (grammar.cma or
+If you add a dependency to a Coq camlp5 extension (grammar.cma or
 q_constr.cmo), then see sections ".ml4 files" and "new files".
 
 Cleaning Targets
@@ -127,7 +127,7 @@ of a grammar extension via a line of the form:
 
 The use of (*i camlp4use: ... i*) to mention uses of standard
 extension such as IFDEF has also been discontinued, the Makefile now
-always calls camlp4 with pa_macros.cmo and a few others by default.
+always calls camlp5 with pa_macros.cmo and a few others by default.
 
 For debugging a Coq grammar extension, it could be interesting
 to use the READABLE_ML4=1 option, otherwise the generated .ml are
@@ -143,7 +143,9 @@ file list(s):
    These files are also used by the experimental ocamlbuild plugin,
    which is quite touchy about them : be careful with order,
    duplicated entries, whitespace errors, and do not mention .mli there.
- - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
+   If module B depends on module A, then B should be after A in the .mllib
+   file.
+- For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
  - The definitions in Makefile.common might have to be adapted too.
  - If your file needs a specific rule, add it to Makefile.build
 
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index aef62b0092..ab78b0956f 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -20,6 +20,14 @@ General deprecation
   removed. Please, make sure your plugin is warning-free in 8.7 before
   trying to port it over 8.8.
 
+Proof engine
+
+  Due to the introduction of `EConstr` in 8.7, it is not necessary to
+  track "goal evar normal form status" anymore, thus the type `'a
+  Proofview.Goal.t` loses its ghost argument. This may introduce some
+  minor incompatibilities at the typing level. Code-wise, things
+  should remain the same.
+
 We removed the following functions:
 
 - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context`
@@ -41,6 +49,14 @@ We changed the type of the following functions:
   a functional way. The old style of passing `evar_map`s as references
   is not supported anymore.
 
+Changes in the abstract syntax tree:
+
+- The practical totality of the AST has been nodified using
+  `CAst.t`. This means that all objects coming from parsing will be
+  indeed wrapped in a `CAst.t`. `Loc.located` is on its way to
+  deprecation. Some minor interfaces changes have resulted from
+  this.
+
 We have changed the representation of the following types:
 
 - `Lib.object_prefix` is now a record instead of a nested tuple.
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index 2dbd132da7..b3d49b7e56 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -25,7 +25,7 @@ intf :
 
 grammar :
 
- Camlp4 syntax extensions. The file grammar/grammar.cma is used
+ Camlp5 syntax extensions. The file grammar/grammar.cma is used
  to pre-process .ml4 files containing EXTEND constructions,
  either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND.
  This grammar.cma incorporates many files from other directories
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
index 0003a2c217..c48c2d5d16 100644
--- a/dev/doc/setup.txt
+++ b/dev/doc/setup.txt
@@ -41,15 +41,15 @@ Building coqtop:
   cd ~/git/coq
   git checkout trunk
   make distclean
-  ./configure -annotate -local
+  ./configure -profile devel
   make clean
   make -j4 coqide printers
 
-The "-annotate" option is essential when one wants to use Merlin.
+The "-profile devel" enables all options recommended for developers (like
+warnings, support for Merlin, etc).  Moreover Coq is configured so that
+it can be run without installing it (i.e. from the current directory).
 
-The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install
-
-Then check if
+Once the compilation is over check if
 - bin/coqtop
 - bin/coqide
 behave as expected.