Imported Upstream version 8.8.2upstream/8.8.2

20 files changed, 2268 insertions, 777 deletions

diff --git a/dev/doc/COMPATIBILITY b/dev/doc/COMPATIBILITY
new file mode 100644
index 00000000..a81afca3
--- /dev/null
+++ b/dev/doc/COMPATIBILITY
@@ -0,0 +1,201 @@
+Note: this file isn't used anymore. Incompatibilities are documented
+as part of CHANGES.
+
+Potential sources of incompatibilities between Coq V8.6 and V8.7
+----------------------------------------------------------------
+
+- Extra superfluous names in introduction patterns may now raise an
+  error rather than a warning when the superfluous name is already in
+  use. The easy fix is to remove the superfluous name.
+
+Potential sources of incompatibilities between Coq V8.5 and V8.6
+----------------------------------------------------------------
+
+Symptom: An obligation generated by Program or an abstracted subproof
+has different arguments.
+Cause: Set Shrink Abstract and Set Shrink Obligations are on by default
+and the subproof does not use the argument.
+Remedy:
+- Adapt the script.
+- Write an explicit lemma to prove the obligation/subproof and use it
+  instead (compatible with 8.4).
+- Unset the option for the program/proof the obligation/subproof originates
+  from.
+
+Symptom: In a goal, order of hypotheses, or absence of an equality of
+the form "x = t" or "t = x", or no unfolding of a local definition.
+Cause: This might be connected to a number of fixes in the tactic
+"subst". The former behavior can be reactivated by issuing "Unset
+Regular Subst Tactic".
+  
+Potential sources of incompatibilities between Coq V8.4 and V8.5
+----------------------------------------------------------------
+
+* List of typical changes to be done to adapt files from Coq 8.4 *
+* to Coq 8.5 when not using compatibility option "-compat 8.4".  *
+
+Symptom: "The reference omega was not found in the current environment".
+Cause: "Require Omega" does not import the tactic "omega" any more
+Possible solutions:
+- use "Require Import OmegaTactic" (not compatible with 8.4)
+- use "Require Import Omega" (compatible with 8.4)
+- add definition "Ltac omega := Coq.omega.Omega.omega."
+  
+Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective)
+Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives
+Possible solutions:
+- use "dintuition" instead; it is stronger than "intuition" and works
+  uniformly on non standard connectives, such as n-ary conjunctions or disjunctions
+  (not compatible with 8.4)
+- do the script differently
+
+Symptom: The constructor foo (in type bar) expects n arguments.
+Cause: parameters must now be given in patterns
+Possible solutions:
+- use option "Set Asymmetric Patterns" (compatible with 8.4)
+- add "_" for the parameters (not compatible with 8.4)
+- turn the parameters into implicit arguments (compatible with 8.4)
+
+Symptom: "NPeano.Nat.foo" not existing anymore
+Possible solutions:
+- use "Nat.foo" instead
+
+Symptom: typing problems with proj1_sig or similar
+Cause: coercion from sig to sigT and similar coercions have been
+  removed so as to make the initial state easier to understand for
+  beginners
+Solution: change proj1_sig into projT1 and similarly (compatible with 8.4)
+
+* Other detailed changes *
+
+(see also file CHANGES)
+
+- options for *coq* compilation (see below for ocaml).
+
+** [-I foo] is now deprecated and will not add directory foo to the
+   coq load path (only for ocaml, see below). Just replace [-I foo] by
+   [-Q foo ""] in your project file and re-generate makefile. Or
+   perform the same operation directly in your makefile if you edit it
+   by hand.
+
+** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq
+   load path.
+
+** Option [-I foo -as bar] is unchanged but discouraged unless you
+   compile ocaml code. Use -Q foo bar instead.
+
+  for more details: file CHANGES or section "Customization at launch
+  time" of the reference manual.
+
+- Command line options for ocaml  Compilation of ocaml code (plugins) 
+
+** [-I foo] is *not* deprecated to add foo to the ocaml load path.
+
+** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to
+   the coq load path with logical name bar (shortcut for -I foo -Q foo
+   bar).
+
+  for more details: file CHANGES or section "Customization at launch
+  time" of the reference manual.
+
+- Universe Polymorphism.
+
+- Refinement, unification and tactics are now aware of universes,
+  resulting in more localized errors. Universe inconsistencies 
+  should no more get raised at Qed time but during the proof.
+  Unification *always* produces well-typed substitutions, hence
+  some rare cases of unifications that succeeded while producing
+  ill-typed terms before will now fail.
+  
+- The [change p with c] tactic semantics changed, now typechecking 
+  [c] at each matching occurrence [t] of the pattern [p], and 
+  converting [t] with [c].
+  
+- Template polymorphic inductive types: the partial application 
+  of a template polymorphic type (e.g. list) is not polymorphic.
+  An explicit parameter application (e.g [fun A => list A]) or
+  [apply (list _)] will result in a polymorphic instance.
+
+- The type inference algorithm now takes opacity of constants into
+  account. This may have effects on tactics using type inference
+  (e.g. induction). Extra "Transparent" might have to be added to
+  revert opacity of constants.
+
+Type classes.
+
+- When writing an Instance foo : Class A := {| proj := t |} (note the
+  vertical bars), support for typechecking the projections using the
+  type information and switching to proof mode is no longer available.
+  Use { } (without the vertical bars) instead.
+
+Tactic abstract.
+
+- Auxiliary lemmas generated by the abstract tactic are removed from
+  the global environment and inlined in the proof term when a proof
+  is ended with Qed.  The behavior of 8.4 can be obtained by ending
+  proofs with "Qed exporting" or "Qed exporting ident, .., ident".
+
+Potential sources of incompatibilities between Coq V8.3 and V8.4
+----------------------------------------------------------------
+
+(see also file CHANGES)
+
+The main known incompatibilities between 8.3 and 8.4 are consequences
+of the following changes:
+
+- The reorganization of the library of numbers:
+
+  Several definitions have new names or are defined in modules of
+  different names, but a special care has been taken to have this
+  renaming transparent for the user thanks to compatibility notations.
+
+  However some definitions have changed, what might require some
+  adaptations. The most noticeable examples are:
+  - The "?=" notation which now bind to Pos.compare rather than former
+    Pcompare (now Pos.compare_cont).
+  - Changes in names may induce different automatically generated
+    names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec").
+  - Z.add has a new definition, hence, applying "simpl" on subterms of
+    its body might give different results than before.
+  - BigN.shiftl and BigN.shiftr have reversed arguments order, the
+    power function in BigN now takes two BigN.
+
+- Other changes in libraries:
+
+  - The definition of functions over "vectors" (list of fixed length)
+    have changed.
+  - TheoryList.v has been removed.
+
+- Slight changes in tactics:
+
+  - Less unfolding of fixpoints when applying destruct or inversion on
+    a fixpoint hiding an inductive type (add an extra call to simpl to
+    preserve compatibility).
+  - Less unexpected local definitions when applying "destruct"
+    (incompatibilities solvable by adapting name hypotheses).
+  - Tactic "apply" might succeed more often, e.g. by now solving
+    pattern-matching of the form ?f x y = g(x,y) (compatibility
+    ensured by using "Unset Tactic Pattern Unification"), but also
+    because it supports (full) betaiota (using "simple apply" might
+    then help).
+  - Tactic autorewrite does no longer instantiate pre-existing
+    existential variables.
+  - Tactic "info" is now available only for auto, eauto and trivial.
+
+- Miscellaneous changes:
+
+  - The command "Load" is now atomic for backtracking (use "Unset
+    Atomic Load" for compatibility).
+
+
+Incompatibilities beyond 8.4...
+
+- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is
+  now "A -> (B <-> C)"
+
+- Tactics: tauto and intuition no longer accidentally destruct binary
+  connectives or records other than and, or, prod, sum, iff. In most
+  of cases, dtauto or dintuition, though stronger than 8.3 tauto and
+  8.3 intuition will provide compatibility.
+
+- "Solve Obligations using" is now "Solve Obligations with".
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index fefcb093..abba1342 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.
@@ -74,25 +74,25 @@ The Makefile is separated in several files :
 - Makefile.doc : specific rules for compiling the documentation.
 
 
-FIND_VCS_CLAUSE
+FIND_SKIP_DIRS
 ---------------
 
-The recommended style of using FIND_VCS_CLAUSE is for example
+The recommended style of using FIND_SKIP_DIRS is for example
 
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print
 
 1)
 The parentheses even in the one-criteria case is so that if one adds
 other conditions, e.g. change the first example to the second
 
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
 
 one is not tempted to write
 
- find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print
+ find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print
 
-because this will not necessarily work as expected; $(FIND_VCS_CLAUSE)
+because this will not necessarily work as expected; $(FIND_SKIP_DIRS)
 ends with an -or, and how it combines with what comes later depends on
 operator precedence and all that. Much safer to override it with
 parentheses.
@@ -105,13 +105,13 @@ As to the -print at the end, yes it is necessary. Here's why.
 You are used to write:
  find . -name '*.example'
 and it works fine. But the following will not:
- find . $(FIND_VCS_CLAUSE) -name '*.example'
-it will also list things directly matched by FIND_VCS_CLAUSE
+ find . $(FIND_SKIP_DIRS) -name '*.example'
+it will also list things directly matched by FIND_SKIP_DIRS
 (directories we want to prune, in which we don't want to find
 anything). C'est subtil... Il y a effectivement un -print implicite à
 la fin, qui fait que la commande habituelle sans print fonctionne
 bien, mais dès que l'on introduit d'autres commandes dans le lot (le
--prune de FIND_VCS_CLAUSE), ça se corse à cause d'histoires de
+-prune de FIND_SKIP_DIRS), ça se corse à cause d'histoires de
 parenthèses du -print implicite par rapport au parenthésage dans la
 forme recommandée d'utilisation:
 
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 873adc1b..fd310161 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.txt b/dev/doc/changes.md
index 3de938d7..ab78b095 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.md
@@ -1,28 +1,433 @@
-=========================================
-= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
-=========================================
+## Changes between Coq 8.7 and Coq 8.8
 
-** Parsing **
+### Bug tracker
 
-Pcoq.parsable now takes an extra optional filename argument so as to
+As of 18/10/2017, Coq uses [GitHub issues](https://github.com/coq/coq/issues)
+as bug tracker.
+Old bug reports were migrated from Bugzilla to GitHub issues using
+[this migration script](https://gist.github.com/Zimmi48/d923e52f64fe17c72852d9c148bfcdc6#file-bugzilla2github)
+as detailed in [this blog post](https://www.theozimmermann.net/2017/10/bugzilla-to-github/).
+
+All the bugs with a number below 1154 had to be renumbered, you can find
+a correspondence table [here](/dev/bugzilla2github_stripped.csv).
+All the other bugs kept their number.
+
+### ML API
+
+General deprecation
+
+- All functions marked [@@ocaml.deprecated] in 8.7 have been
+  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`
+  instead. The returned term contains De Bruijn universe variables. If you don't
+  depend on universes being instantiated, simply drop the context.
+
+- `Universes.unsafe_type_of_global`: same as above with
+  `Global.type_of_global_in_context`
+
+We changed the type of the following functions:
+
+- `Global.body_of_constant_body`: now also returns the abstract universe context.
+  The returned term contains De Bruijn universe variables.
+
+- `Global.body_of_constant`: same as above.
+
+- `Constrinterp.*` generally, many functions that used to take an
+  `evar_map ref` have been now switched to functions that will work in
+  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.
+
+Some tactics and related functions now support static configurability, e.g.:
+
+- injectable, dEq, etc. takes an argument ~keep_proofs which,
+  - if None, tells to behave as told with the flag Keep Proof Equalities
+  - if Some b, tells to keep proof equalities iff b is true
+
+Declaration of printers for arguments used only in vernac command
+
+- It should now use "declare_extra_vernac_genarg_pprule" rather than
+  "declare_extra_genarg_pprule", otherwise, a failure at runtime might
+  happen. An alternative is to register the corresponding argument as
+  a value, using "Geninterp.register_val0 wit None".
+
+### STM API
+
+The STM API has seen a general overhaul. The main change is the
+introduction of a "Coq document" type, which all operations now take
+as a parameter. This effectively functionalize the STM API and will
+allow in the future to handle several documents simultaneously.
+
+The main remarkable point is that key implicit global parameters such
+as load-paths and required modules are now arguments to the document
+creation function. This helps enforcing some key invariants.
+
+### XML IDE Protocol
+
+- Before 8.8, `Query` only executed the first command present in the
+ `query` string; starting with 8.8, the caller may include several
+ statements. This is useful for instance for temporarily setting an
+ option and then executing a command.
+
+## Changes between Coq 8.6 and Coq 8.7
+
+### Ocaml
+
+Coq is compiled with `-safe-string` enabled and requires plugins to do
+the same. This means that code using `String` in an imperative way
+will fail to compile now. They should switch to `Bytes.t`
+
+Configure supports passing flambda options, use `-flambda-opts OPTS`
+with a flambda-enabled Ocaml to tweak the compilation to your taste.
+
+### ML API
+
+- Added two functions for declaring hooks to be executed in reduction
+functions when some given constants are traversed:
+
+  * `declare_reduction_effect`: to declare a hook to be applied when some
+  constant are visited during the execution of some reduction functions
+  (primarily cbv).
+
+  * `set_reduction_effect`: to declare a constant on which a given effect
+  hook should be called.
+
+- We renamed the following functions:
+
+  ```
+  Context.Rel.Declaration.fold   -> Context.Rel.Declaration.fold_constr
+  Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr
+  Printer.pr_var_list_decl       -> Printer.pr_compacted_decl
+  Printer.pr_var_decl            -> Printer.pr_named_decl
+  Nameops.lift_subscript         -> Nameops.increment_subscript
+  ```
+
+- We removed the following functions:
+
+  * `Termops.compact_named_context_reverse`: practical substitute is `Termops.compact_named_context`.
+  * `Namegen.to_avoid`: equivalent substitute is `Names.Id.List.mem`.
+
+- We renamed the following modules:
+
+  * `Context.ListNamed` -> `Context.Compacted`
+
+- The following type aliases where removed
+
+  * `Context.section_context`: it was just an alias for `Context.Named.t` which is still available.
+
+- The module `Constrarg` was merged into `Stdarg`.
+
+- The following types have been moved and modified:
+
+  * `local_binder` -> `local_binder_expr`
+  * `glob_binder` merged with `glob_decl`
+
+- The following constructors have been renamed:
+
+  ```
+  LocalRawDef -> CLocalDef
+  LocalRawAssum -> CLocalAssum
+  LocalPattern -> CLocalPattern
+  ```
+
+- In `Constrexpr_ops`:
+
+  Deprecating `abstract_constr_expr` in favor of `mkCLambdaN`, and
+  `prod_constr_expr` in favor of `mkCProdN`. Note: the first ones were
+  interpreting `(x y z:_)` as `(x:_) (y:_) (z:_)` while the second
+  ones were preserving the original sharing of the type.
+
+- In `Nameops`:
+
+  The API has been made more uniform. New combinators added in the
+  `Name` space name. Function `out_name` now fails with `IsAnonymous`
+  rather than with `Failure "Nameops.out_name"`.
+
+- Location handling and AST attributes:
+
+  Location handling has been reworked. First, `Loc.ghost` has been
+  removed in favor of an option type, all objects carrying an optional
+  source code location have been switched to use `Loc.t option`.
+
+  Storage of location information has been also refactored. The main
+  datatypes representing Coq AST (`constrexpr`, `glob_expr`) have been
+  switched to a generic "node with attributes" representation `'a
+  CAst.ast`, which is a record of the form:
+
+  ```ocaml
+  type 'a ast = private {
+    v   : 'a;
+    loc : Loc.t option;
+    ...
+  }
+  ```
+  consumers of AST nodes are recommended to use accessor-based pattern
+  matching `{ v; loc }` to destruct `ast` object. Creation is done
+  with `CAst.make ?loc obj`, where the attributes are optional. Some
+  convenient combinators are provided in the module. A typical match:
+
+  ```ocaml
+  | CCase(loc, a1) -> CCase(loc, f a1)
+  ```
+
+  is now done as:
+  ```ocaml
+  | { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1)
+
+  ```
+  or even better, if plan to preserve the attributes you can wrap your
+  top-level function in `CAst.map` to have:
+
+  ```ocaml
+  | CCase(a1) -> CCase(f a1)
+  ```
+
+  This scheme based on records enables easy extensibility of the AST
+  node type without breaking compatibility.
+
+  Not all objects carrying a location have been converted to the
+  generic node representation, some of them may be converted in the
+  future, for some others the abstraction is not just worth it.
+
+  Thus, we still maintain a `'a Loc.located == Loc.t option * a'`,
+  tuple type which should be treated as private datatype (ok to match
+  against, but forbidden to manually build), and it is mandatory to
+  use it for objects that carry a location. This policy has been
+  implemented in the whole code base. Matching a located object hasn't
+  changed, however, `Loc.tag ?loc obj` must be used to build one.
+
+- In `GOption`:
+
+  Support for non-synchronous options has been removed. Now all
+  options are handled as a piece of normal document state, and thus
+  passed to workers, etc... As a consequence, the field
+  `Goptions.optsync` has been removed.
+
+- In `Coqlib` / reference location:
+
+  We have removed from Coqlib functions returning `constr` from
+  names. Now it is only possible to obtain references, that must be
+  processed wrt the particular needs of the client.
+  We have changed in constrintern the functions returnin `constr` as
+  well to return global references instead.
+
+  Users of `coq_constant/gen_constant` can do
+  `Universes.constr_of_global (find_reference dir r)` _however_ note
+  the warnings in the `Universes.constr_of_global` in the
+  documentation. It is very likely that you were previously suffering
+  from problems with polymorphic universes due to using
+  `Coqlib.coq_constant` that used to do this. You must rather use
+  `pf_constr_of_global` in tactics and `Evarutil.new_global` variants
+  when constructing terms in ML (see univpoly.txt for more information).
+
+### Tactic API
+
+- `pf_constr_of_global` now returns a tactic instead of taking a continuation.
+  Thus it only generates one instance of the global reference, and it is the
+  caller's responsibility to perform a focus on the goal.
+
+- `pf_global`, `construct_reference`, `global_reference`,
+  `global_reference_in_absolute_module` now return a `global_reference`
+  instead of a `constr`.
+
+- The `tclWEAK_PROGRESS` and `tclNOTSAMEGOAL` tacticals were removed. Their usecase
+  was very specific. Use `tclPROGRESS` instead.
+
+- New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows
+  to iterate a non-unit tactic on all goals and access their returned values.
+
+- The unsafe flag of the `Refine.refine` function and its variants has been
+  renamed and dualized into typecheck and has been made mandatory.
+
+### Ltac API
+
+Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
+important things:
+
+- `Pcoq.Tactic` -> `Pltac`
+- `Constrarg.wit_tactic` -> `Tacarg.wit_tactic`
+- `Constrarg.wit_ltac` -> `Tacarg.wit_ltac`
+- API below `ltac/` that accepted a *`_tactic_expr` now accept a *`_generic_argument`
+  instead
+- Some printing functions were moved from `Pptactic` to `Pputils`
+- A part of `Tacexpr` has been moved to `Tactypes`
+- The `TacFun` tactic expression constructor now takes a `Name.t list` for the
+  variable list rather than an `Id.t option list`.
+
+The folder itself has been turned into a plugin. This does not change much,
+but because it is a packed plugin, it may wreak havoc for third-party plugins
+depending on any module defined in the `ltac/` directory. Namely, even if
+everything looks OK at compile time, a plugin can fail to load at link time
+because it mistakenly looks for a module `Foo` instead of `Ltac_plugin.Foo`, with
+an error of the form:
+
+```
+Error: while loading myplugin.cmxs, no implementation available for Foo.
+```
+
+In particular, most `EXTEND` macros will trigger this problem even if they
+seemingly do not use any Ltac module, as their expansion do.
+
+The solution is simple, and consists in adding a statement `open Ltac_plugin`
+in each file using a Ltac module, before such a module is actually called. An
+alternative solution would be to fully qualify Ltac modules, e.g. turning any
+call to Tacinterp into `Ltac_plugin.Tacinterp`. Note that this solution does not
+work for `EXTEND` macros though.
+
+### Additional changes in tactic extensions
+
+Entry `constr_with_bindings` has been renamed into
+`open_constr_with_bindings`. New entry `constr_with_bindings` now
+uses type classes and rejects terms with unresolved holes.
+
+### Error handling
+
+- All error functions now take an optional parameter `?loc:Loc.t`. For
+  functions that used to carry a suffix `_loc`, such suffix has been
+  dropped.
+
+- `errorlabstrm` and `error` has been removed in favor of `user_err`.
+
+- The header parameter to `user_err` has been made optional.
+
+### Pretty printing
+
+Some functions have been removed, see pretty printing below for more
+details.
+
+#### Pretty Printing and XML protocol
+
+The type `std_cmdpps` has been reworked and made the canonical "Coq rich
+document type". This allows for a more uniform handling of printing
+(specially in IDEs). The main consequences are:
+
+ - Richpp has been confined to IDE use. Most of previous uses of the
+   `richpp` type should be replaced now by `Pp.std_cmdpps`. Main API
+   has been updated.
+
+ - The XML protocol will send a new message type of `pp`, which should
+   be rendered client-wise.
+
+ - `Set Printing Width` is deprecated, now width is controlled
+   client-side.
+
+ - `Pp_control` has removed. The new module `Topfmt` implements
+   console control for the toplevel.
+
+ - The impure tag system in `Pp` has been removed. This also does away
+   with the printer signatures and functors. Now printers tag
+   unconditionally.
+
+ - The following functions have been removed from `Pp`:
+
+   ```ocaml
+   val stras : int * string -> std_ppcmds
+   val tbrk  : int * int -> std_ppcmds
+   val tab   : unit -> std_ppcmds
+   val pifb  : unit -> std_ppcmds
+   val comment  : int -> std_ppcmds
+   val comments : ((int * int) * string) list ref
+   val eval_ppcmds : std_ppcmds -> std_ppcmds
+   val is_empty : std_ppcmds -> bool
+   val t : std_ppcmds -> std_ppcmds
+   val hb : int -> std_ppcmds
+   val vb : int -> std_ppcmds
+   val hvb : int -> std_ppcmds
+   val hovb : int -> std_ppcmds
+   val tb : unit -> std_ppcmds
+   val close : unit -> std_ppcmds
+   val tclose : unit -> std_ppcmds
+   val open_tag : Tag.t -> std_ppcmds
+   val close_tag : unit -> std_ppcmds
+   val msg_with  : ...
+
+   module Tag
+   ```
+
+### Stm API
+
+- We have streamlined the `Stm` API, now `add` and `query` take a
+  `coq_parsable` instead a `string` so clients can have more control
+  over their input stream. As a consequence, their types have been
+  modified.
+
+- The main parsing entry point has also been moved to the
+  `Stm`. Parsing is considered a synchronous operation so it will
+  either succeed or raise an exception.
+
+- `Feedback` is now only emitted for asynchronous operations. As a
+  consequence, it always carries a valid stateid and the type has
+  changed to accommodate that.
+
+- A few unused hooks were removed due to cleanups, no clients known.
+
+### Toplevel and Vernacular API
+
+- The components related to vernacular interpretation have been moved
+  to their own folder `vernac/` whereas toplevel now contains the
+  proper toplevel shell and compiler.
+
+- Coq's toplevel has been ported to directly use the common `Stm`
+  API. The signature of a few functions has changed as a result.
+
+### XML Protocol
+
+- The legacy `Interp` call has been turned into a noop.
+
+- The `query` call has been modified, now it carries a mandatory
+  `route_id` integer parameter, that associated the result of such
+  query with its generated feedback.
+
+## Changes between Coq 8.5 and Coq 8.6
+
+### Parsing
+
+`Pcoq.parsable` now takes an extra optional filename argument so as to
 bind locations to a file name when relevant.
 
-** Files **
+### Files
 
 To avoid clashes with OCaml's compiler libs, the following files were renamed:
+
+```
 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/
+All IDE-specific files, including the XML protocol have been moved to `ide/`
 
-** Reduction functions **
+### Reduction functions
 
-In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX,
-fCOFIX.
+In `closure.ml`, we introduced the more precise reduction flags `fMATCH`, `fFIX`,
+`fCOFIX`.
 
 We renamed the following functions:
 
+```
 Closure.betadeltaiota -> Closure.all
 Closure.betadeltaiotanolet -> Closure.allnolet
 Reductionops.beta -> Closure.beta
@@ -49,9 +454,11 @@ Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
 Reductionops.whd_eta -> Reductionops.shrink_eta
 Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
 Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all
+```
 
 And removed the following ones:
 
+```
 Reductionops.whd_betaetalet
 Reductionops.whd_betaetalet_stack
 Reductionops.whd_betaetalet_state
@@ -61,15 +468,16 @@ Reductionops.whd_betadeltaeta
 Reductionops.whd_betadeltaiotaeta_stack
 Reductionops.whd_betadeltaiotaeta_state
 Reductionops.whd_betadeltaiotaeta
+```
 
-In intf/genredexpr.mli, fIota was replaced by FMatch, FFix and
-FCofix. Similarly, rIota was replaced by rMatch, rFix and rCofix.
+In `intf/genredexpr.mli`, `fIota` was replaced by `FMatch`, `FFix` and
+`FCofix`. Similarly, `rIota` was replaced by `rMatch`, `rFix` and `rCofix`.
 
-** Notation_ops **
+### Notation_ops
 
-Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr.
+Use `Glob_ops.glob_constr_eq` instead of `Notation_ops.eq_glob_constr`.
 
-** Logging and Pretty Printing: **
+### Logging and Pretty Printing
 
 * Printing functions have been removed from `Pp.mli`, which is now a
   purely pretty-printing interface. Functions affected are:
@@ -98,7 +506,7 @@ val message     : string -> unit
 
 * Feedback related functions and definitions have been moved to the
   `Feedback` module. `message_level` has been renamed to
-  level. Functions moved from Pp to Feedback are:
+  level. Functions moved from `Pp` to `Feedback` are:
 
 ```` ocaml
 val set_logger      : logger -> unit
@@ -143,12 +551,13 @@ val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
 val get_id_for_feedback : unit -> edit_or_state_id * route_id
 ````
 
-** Kernel API changes **
+### Kernel API changes
 
-- The interface of the Context module was changed.
+- The interface of the `Context` module was changed.
   Related types and functions were put in separate submodules.
   The mapping from old identifiers to new identifiers is the following:
 
+    ```
     Context.named_declaration            --->  Context.Named.Declaration.t
     Context.named_list_declaration       --->  Context.NamedList.Declaration.t
     Context.rel_declaration              --->  Context.Rel.Declaration.t
@@ -190,123 +599,148 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id
     Context.rel_context_length           --->  Context.Rel.length
     Context.rel_context_nhyps            --->  Context.Rel.nhyps
     Context.rel_context_tags             --->  Context.Rel.to_tags
+    ```
 
 - Originally, rel-context was represented as:
 
-    Context.rel_context = Names.Name.t * Constr.t option * Constr.t
+    ```ocaml
+    type Context.rel_context = Names.Name.t * Constr.t option * Constr.t
+    ```
 
   Now it is represented as:
 
-    Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t
-	                      | LocalDef of Names.Name.t * Constr.t * Constr.t
- 
+    ```ocaml
+    type Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t
+                                   | LocalDef of Names.Name.t * Constr.t * Constr.t
+    ```
+
 - Originally, named-context was represented as:
 
-    Context.named_context = Names.Id.t * Constr.t option * Constr.t
+    ```ocaml
+    type Context.named_context = Names.Id.t * Constr.t option * Constr.t
+    ```
 
   Now it is represented as:
 
-    Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t
-	                        | LocalDef of Names.Id.t * Constr.t * Constr.t
+    ```ocaml
+    type Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t
+                                     | LocalDef of Names.Id.t * Constr.t * Constr.t
+    ```
 
-- The various EXTEND macros do not handle specially the Coq-defined entries
+- The various `EXTEND` macros do not handle specially the Coq-defined entries
   anymore. Instead, they just output a name that have to exist in the scope
-  of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for
-  variables "$name" of type Gram.entry, while the parsing rules of
-  (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will
-  look for variables "wit_$name" of type Genarg.genarg_type. The small DSL
+  of the ML code. The parsing rules (`VERNAC`) `ARGUMENT EXTEND` will look for
+  variables `$name` of type `Gram.entry`, while the parsing rules of
+  (`VERNAC COMMAND` | `TACTIC`) `EXTEND`, as well as the various `TYPED AS` clauses will
+  look for variables `wit_$name` of type `Genarg.genarg_type`. The small DSL
   for constructing compound entries still works over this scheme. Note that in
-  the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound
+  the case of (`VERNAC`) `ARGUMENT EXTEND`, the name of the argument entry is bound
   in the parsing rules, so beware of recursive calls.
   
-  For example, to get "wit_constr" you must "open Constrarg" at the top of the file.
+  For example, to get `wit_constr` you must `open Constrarg` at the top of the file.
 
-- Evarutil was split in two parts. The new Evardefine file exposes functions
-define_evar_* mostly used internally in the unification engine.
+- `Evarutil` was split in two parts. The new `Evardefine` file exposes functions
+  `define_evar_`* mostly used internally in the unification engine.
 
-- The Refine module was move out of Proofview.
+- The `Refine` module was moved out of `Proofview`.
 
+    ```
     Proofview.Refine.* --->  Refine.*
+    ```
 
-- A statically monotonous evarmap type was introduced in Sigma. Not all the API
+- A statically monotonic evarmap type was introduced in `Sigma`. Not all the API
   has been converted, so that the user may want to use compatibility functions
-  Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when
+  `Sigma.to_evar_map` and `Sigma.Unsafe.of_evar_map` or `Sigma.Unsafe.of_pair` when
   needed. Code can be straightforwardly adapted in the following way:
 
+  ```ocaml
   let (sigma, x1) = ... in
   ...
   let (sigma, xn) = ... in
   (sigma, ans)
+  ```
 
   should be turned into:
 
+  ```ocaml
   open Sigma.Notations
 
   let Sigma (x1, sigma, p1) = ... in
   ...
   let Sigma (xn, sigma, pn) = ... in
   Sigma (ans, sigma, p1 +> ... +> pn)
+  ```
   
   Examples of `Sigma.Unsafe.of_evar_map` include:
   
+  ```
   Evarutil.new_evar env (Tacmach.project goal) ty   ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty
+  ```
 
-- The Proofview.Goal.*enter family of functions now takes a polymorphic
+- The `Proofview.Goal.`*`enter` family of functions now takes a polymorphic
   continuation given as a record as an argument.
 
+  ```ocaml
   Proofview.Goal.enter begin fun gl -> ... end
+  ```
 
   should be turned into
 
+  ```ocaml
   open Proofview.Notations
 
   Proofview.Goal.enter { enter = begin fun gl -> ... end }
+  ```
   
 - `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)`      ---> `Tacinterp.Value.of_constr c`
 - `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)`
 - `Pretyping.Termops.mem_named_context`                           ---> `Engine.Termops.mem_named_context_val`
-  (`Global.named_context`                                         ---> `Global.named_context_val`)
-  (`Context.Named.lookup`                                         ---> `Environ.lookup_named_val`)
+- `Global.named_context`                                         ---> `Global.named_context_val`
+- `Context.Named.lookup`                                         ---> `Environ.lookup_named_val`
 
-** Search API **
+### Search API
 
 The main search functions now take a function iterating over the
 results. This allows for clients to use streaming or more economic
 printing.
 
-=========================================
-= CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
-=========================================
+### XML Protocol
+
+- In several places, flat text wrapped in `<string>` tags now appears as structured text inside `<richpp>` tags.
+
+- The "errormsg" feedback has been replaced by a "message" feedback which contains `<feedback\_content>` tag, with a message_level attribute of "error".
 
-** Refactoring : more mli interfaces and simpler grammar.cma **
+## Changes between Coq 8.4 and Coq 8.5
+
+### Refactoring : more mli interfaces and simpler grammar.cma
 
 - A new directory intf/ now contains mli-only interfaces :
 
- Constrexpr : definition of constr_expr, was in Topconstr
- Decl_kinds : now contains binding_kind = Explicit | Implicit
- Evar_kinds : type Evar_kinds.t was previously Evd.hole_kind
- Extend : was parsing/extend.mli
- Genredexpr : regroup Glob_term.red_expr_gen and Tacexpr.glob_red_flag
- Glob_term  : definition of glob_constr
- Locus : definition of occurrences and stuff about clauses
- Misctypes : intro_pattern_expr, glob_sort, cast_type, or_var, ...
- Notation_term : contains notation_constr, was Topconstr.aconstr
- Pattern : contains constr_pattern
- Tacexpr : was tactics/tacexpr.ml
- Vernacexpr : was toplevel/vernacexpr.ml
+  * `Constrexpr` : definition of `constr_expr`, was in `Topconstr`
+  * `Decl_kinds` : now contains `binding_kind = Explicit | Implicit`
+  * `Evar_kinds` : type `Evar_kinds.t` was previously `Evd.hole_kind`
+  * `Extend` : was `parsing/extend.mli`
+  * `Genredexpr` : regroup `Glob_term.red_expr_gen` and `Tacexpr.glob_red_flag`
+  * `Glob_term`  : definition of `glob_constr`
+  * `Locus` : definition of occurrences and stuff about clauses
+  * `Misctypes` : `intro_pattern_expr`, `glob_sort`, `cast_type`, `or_var`, ...
+  * `Notation_term` : contains `notation_constr`, was `Topconstr.aconstr`
+  * `Pattern` : contains `constr_pattern`
+  * `Tacexpr` : was `tactics/tacexpr.ml`
+  * `Vernacexpr` : was `toplevel/vernacexpr.ml`
 
 - Many files have been divided :
 
- vernacexpr: vernacexpr.mli + Locality
- decl_kinds: decl_kinds.mli + Kindops
- evd: evar_kinds.mli + evd
- tacexpr: tacexpr.mli + tacops
- glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops
- topconstr: constrexpr.mli + constrexpr_ops
-            + notation_expr.mli + notation_ops + topconstr
- pattern: pattern.mli + patternops
- libnames: libnames (qualid, reference) + globnames (global_reference)
- egrammar: egramml + egramcoq
+  * vernacexpr: vernacexpr.mli + Locality
+  * decl_kinds: decl_kinds.mli + Kindops
+  * evd: evar_kinds.mli + evd
+  * tacexpr: tacexpr.mli + tacops
+  * glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops
+  * topconstr: constrexpr.mli + constrexpr_ops
+              + notation_expr.mli + notation_ops + topconstr
+  * pattern: pattern.mli + patternops
+  * libnames: libnames (qualid, reference) + globnames (global_reference)
+  * egrammar: egramml + egramcoq
 
 - New utility files : miscops (cf. misctypes.mli) and
   redops (cf genredexpr.mli).
@@ -355,11 +789,11 @@ printing.
   letin_pat_tac do not accept a type anymore
 
 - New file find_subterm.ml for gathering former functions
-  subst_closed_term_occ_modulo, subst_closed_term_occ_decl (which now
-  take and outputs also an evar_map), and
-  subst_closed_term_occ_modulo, subst_closed_term_occ_decl_modulo (now
-  renamed into replace_term_occ_modulo and
-  replace_term_occ_decl_modulo).
+  `subst_closed_term_occ_modulo`, `subst_closed_term_occ_decl` (which now
+  take and outputs also an `evar_map`), and
+  `subst_closed_term_occ_modulo`, `subst_closed_term_occ_decl_modulo` (now
+  renamed into `replace_term_occ_modulo` and
+  `replace_term_occ_decl_modulo`).
 
 - API of Inductiveops made more uniform (see commit log or file itself).
 
@@ -373,36 +807,34 @@ printing.
 - All functions taking an env and a sigma (or an evdref) now takes the
   env first.
 
-=========================================
-= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
-=========================================
+## Changes between Coq 8.3 and Coq 8.4
 
-** Functions in unification.ml have now the evar_map coming just after the env
+- Functions in unification.ml have now the evar_map coming just after the env
 
-** Removal of Tacinterp.constr_of_id **
+- Removal of Tacinterp.constr_of_id
 
 Use instead either global_reference or construct_reference in constrintern.ml.
 
-** Optimizing calls to Evd functions **
+- Optimizing calls to Evd functions
 
 Evars are split into defined evars and undefined evars; for
 efficiency, when an evar is known to be undefined, it is preferable to
 use specific functions about undefined evars since these ones are
 generally fewer than the defined ones.
 
-** Type changes in TACTIC EXTEND rules **
+- Type changes in TACTIC EXTEND rules
 
 Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type
 glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first
 component is kept, the second one can be obtained via
 Tacinterp.eval_tactic.
 
-** ARGUMENT EXTEND **
+- ARGUMENT EXTEND
 
 It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED
 in ARGUMENT EXTEND statements.
 
-** Renaming of rawconstr to glob_constr **
+- Renaming of rawconstr to glob_constr
 
 The "rawconstr" type has been renamed to "glob_constr" for
 consistency. The "raw" in everything related to former rawconstr has
@@ -412,62 +844,67 @@ scripts to migrate code using Coq's internals, see commits 13743,
 2010) in Subversion repository. Contribs have been fixed too, and
 commit messages there might also be helpful for migrating.
 
-=========================================
-= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
-=========================================
+## Changes between Coq 8.2 and Coq 8.3
 
-** Light cleaning in evarutil.ml **
+### Light cleaning in evaruil.ml
 
 whd_castappevar is now whd_head_evar
 obsolete whd_ise disappears
 
-** Restructuration of the syntax of binders **
+### Restructuration of the syntax of binders
 
+```
 binders_let -> binders
 binders_let_fixannot -> binders_fixannot
 binder_let -> closed_binder (and now covers only bracketed binders)
 binder was already obsolete and has been removed
+```
 
-** Semantical change of h_induction_destruct **
+### Semantical change of h_induction_destruct
 
 Warning, the order of the isrec and evar_flag was inconsistent and has
 been permuted. Tactic induction_destruct in tactics.ml is unchanged.
 
-** Internal tactics renamed
+### Internal tactics renamed
 
 There is no more difference between bindings and ebindings. The
 following tactics are therefore renamed
 
+```
 apply_with_ebindings_gen -> apply_with_bindings_gen
 left_with_ebindings -> left_with_bindings
 right_with_ebindings -> right_with_bindings
 split_with_ebindings -> split_with_bindings
+```
 
 and the following tactics are removed
 
-apply_with_ebindings (use instead apply_with_bindings)
-eapply_with_ebindings (use instead eapply_with_bindings)
+ - apply_with_ebindings (use instead apply_with_bindings)
+ - eapply_with_ebindings (use instead eapply_with_bindings)
 
-** Obsolete functions in typing.ml
+### Obsolete functions in typing.ml
 
 For mtype_of, msort_of, mcheck, now use type_of, sort_of, check
 
-** Renaming functions renamed
+### Renaming functions renamed
 
+```
 concrete_name -> compute_displayed_name_in
 concrete_let_name -> compute_displayed_let_name_in
 rename_rename_bound_var -> rename_bound_vars_as_displayed
 lookup_name_as_renamed -> lookup_name_as_displayed
 next_global_ident_away true -> next_ident_away_in_goal
 next_global_ident_away false -> next_global_ident_away
+```
 
-** Cleaning in commmand.ml
+### Cleaning in commmand.ml
 
 Functions about starting/ending a lemma are in lemmas.ml
 Functions about inductive schemes are in indschemes.ml
 
 Functions renamed:
 
+```
 declare_one_assumption -> declare_assumption
 declare_assumption -> declare_assumptions
 Command.syntax_definition -> Metasyntax.add_syntactic_definition
@@ -484,15 +921,17 @@ instantiate_type_indrec_scheme -> weaken_sort_scheme
 instantiate_indrec_scheme -> modify_sort_scheme
 make_case_dep, make_case_nodep -> build_case_analysis_scheme
 make_case_gen -> build_case_analysis_scheme_default
+```
 
 Types:
 
 decl_notation -> decl_notation option
 
-** Cleaning in libnames/nametab interfaces
+### Cleaning in libnames/nametab interfaces
 
 Functions:
 
+```
 dirpath_prefix -> pop_dirpath
 extract_dirpath_prefix pop_dirpath_n
 extend_dirpath -> add_dirpath_suffix
@@ -506,17 +945,19 @@ absolute_reference -> global_of_path
 locate_syntactic_definition -> locate_syndef
 path_of_syntactic_definition -> path_of_syndef
 push_syntactic_definition -> push_syndef
+```
 
 Types:
 
 section_path -> full_path
 
-** Cleaning in parsing extensions (commit 12108)
+### Cleaning in parsing extensions (commit 12108)
 
 Many moves and renamings, one new file (Extrawit, that contains wit_tactic).
 
-** Cleaning in tactical.mli
+### Cleaning in tactical.mli
 
+```
 tclLAST_HYP -> onLastHyp
 tclLAST_DECL -> onLastDecl
 tclLAST_NHYPS -> onNLastHypsId
@@ -526,24 +967,21 @@ onLastHyp -> onLastHypId
 onNLastHyps -> onNLastDecls
 onClauses -> onClause
 allClauses -> allHypsAndConcl
+```
 
-+ removal of various unused combinators on type "clause"
-
-=========================================
-= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
-=========================================
+and removal of various unused combinators on type "clause"
 
-A few differences in Coq ML interfaces between Coq V8.1 and V8.2
-================================================================
+## Changes between Coq 8.1 and Coq 8.2
 
-** Datatypes
+### Datatypes
 
 List of occurrences moved from "int list" to "Termops.occurrences" (an
   alias to "bool * int list")
 ETIdent renamed to ETName
 
-** Functions
+### Functions
 
+```
 Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
 Tactics: apply_with_bindings -> apply_with_bindings_wo_evars
 Eauto.simplest_apply -> Hiddentac.h_simplest_apply
@@ -553,98 +991,93 @@ Tactics.true_cut renamed into Tactics.assert_tac
 Constrintern.interp_constrpattern -> intern_constr_pattern
 Hipattern.match_with_conjunction is a bit more restrictive
 Hipattern.match_with_disjunction is a bit more restrictive
+```
 
-** Universe names (univ.mli)
+### Universe names (univ.mli)
 
+ ```ocaml
  base_univ -> type0_univ  (* alias of Set is the Type hierarchy *)
  prop_univ -> type1_univ  (* the type of Set in the Type hierarchy *)
  neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *)
  is_base_univ -> is_type1_univ
  is_empty_univ -> is_lower_univ
+ ```
 
-** Sort names (term.mli)
+### Sort names (term.mli)
 
+  ```
   mk_Set -> set_sort
   mk_Prop -> prop_sort
   type_0 -> type1_sort
-
-=========================================
-= CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
-=========================================
-
-A few differences in Coq ML interfaces between Coq V8.0 and V8.1
-================================================================
-
-** Functions
-
-Util: option_app -> option_map
-Term: substl_decl -> subst_named_decl
-Lib: library_part -> remove_section_part
-Printer: prterm -> pr_lconstr
-Printer: prterm_env -> pr_lconstr_env
-Ppconstr: pr_sort -> pr_rawsort
-Evd: in_dom, etc got standard ocaml names (i.e. mem, etc)
-Pretyping: 
- - understand_gen_tcc and understand_gen_ltac merged into understand_ltac
- - type_constraints can now say typed by a sort (use OfType to get the
-   previous behavior)
-Library: import_library -> import_module
-
-** Constructors
-
-Declarations: mind_consnrealargs -> mind_consnrealdecls
-NoRedun -> NoDup
-Cast and RCast have an extra argument: you can recover the previous
+  ```
+
+## Changes between Coq 8.0 and Coq 8.1
+
+### Functions
+
+- Util: option_app -> option_map
+- Term: substl_decl -> subst_named_decl
+- Lib: library_part -> remove_section_part
+- Printer: prterm -> pr_lconstr
+- Printer: prterm_env -> pr_lconstr_env
+- Ppconstr: pr_sort -> pr_rawsort
+- Evd: in_dom, etc got standard ocaml names (i.e. mem, etc)
+- Pretyping:
+   - understand_gen_tcc and understand_gen_ltac merged into understand_ltac
+   - type_constraints can now say typed by a sort (use OfType to get the
+     previous behavior)
+- Library: import_library -> import_module
+
+### Constructors
+
+ * Declarations: mind_consnrealargs -> mind_consnrealdecls
+ * NoRedun -> NoDup
+ * Cast and RCast have an extra argument: you can recover the previous
   behavior by setting the extra argument to "CastConv DEFAULTcast" and
   "DEFAULTcast" respectively
-Names: "kernel_name" is now "constant" when argument of Term.Const
-Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert
-Tacexpr: TacForward(true,_,_) branched to TacLetTac
+ * Names: "kernel_name" is now "constant" when argument of Term.Const
+ * Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert
+ * Tacexpr: TacForward(true,_,_) branched to TacLetTac
 
-** Modules
+### Modules
 
-module Decl_kinds: new interface
-module Bigint: new interface
-module Tacred spawned module Redexpr
-module Symbols -> Notation
-module Coqast, Ast, Esyntax, Termast, and all other modules related to old
-  syntax are removed
-module Instantiate: integrated to Evd
-module Pretyping now a functor: use Pretyping.Default instead
+ * module Decl_kinds: new interface
+ * module Bigint: new interface
+ * module Tacred spawned module Redexpr
+ * module Symbols -> Notation
+ * module Coqast, Ast, Esyntax, Termast, and all other modules related to old
+   syntax are removed
+ * module Instantiate: integrated to Evd
+ * module Pretyping now a functor: use Pretyping.Default instead
 
-** Internal names
+### Internal names
 
 OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE
 
-** Tactic extensions
+### Tactic extensions
 
-- printers have an extra parameter which is a constr printer at high precedence
-- the tactic printers have an extra arg which is the expected precedence 
-- level is now a precedence in declare_extra_tactic_pprule
-- "interp" functions now of types the actual arg type, not its encapsulation
-  as a generic_argument
+ * printers have an extra parameter which is a constr printer at high precedence
+ *  the tactic printers have an extra arg which is the expected precedence
+ *  level is now a precedence in declare_extra_tactic_pprule
+ * "interp" functions now of types the actual arg type, not its encapsulation
+    as a generic_argument
 
-=========================================
-= CHANGES BETWEEN COQ V7.4 AND COQ V8.0 =
-=========================================
+## Changes between Coq 7.4 and Coq 8.0
 
 See files in dev/syntax-v8
 
 
-==============================================
-= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 =
-==============================================
+## Main changes between Coq 7.4 and Coq 8.0
 
-CHANGES DUE TO INTRODUCTION OF MODULES
-======================================
+### Changes due to introduction of modules
 
-1.Kernel
---------
+#### Kernel
 
   The module level has no effect on constr except for the structure of
 section_path. The type of unique names for constructions (what
 section_path served) is now called a kernel name and is defined by
  
+```ocaml
 type uniq_ident = int * string * dir_path (* int may be enough *)
 type module_path =
   | MPfile of dir_path    (* reference to physical module, e.g. file *)
@@ -671,7 +1104,8 @@ type kernel_name = module_path * dir_path * label
          Def u = ...
        end
        Def x := ... <M>.t ... <N>.O.u ... X.T.b ... L.A.a
- 
+```
+
    <M> and <N> are self-references, X is a bound reference and L is a
 reference to a physical module.
  
@@ -688,14 +1122,13 @@ world.
 module_expr) and kernel/declarations.ml (type module_body and
 module_type_body).                                                              
 
-2. Library
-----------
+#### Library
 
-i) tables 
+1. tables
 [Summaries] - the only change is the special treatment of the
 global environmet.
 
-ii) objects 
+2. objects 
 [Libobject] declares persistent objects, given with methods:
 
    * cache_function specifying how to add the object in the current
@@ -716,25 +1149,25 @@ Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal
 version such as (MPself<Datatypes#1>,[],"Fst") (see above)
 
 
-What happens at the end of an interactive module ?
-==================================================
+#### What happens at the end of an interactive module ?
+
 (or when a file is stored and reloaded from disk)
 
 All summaries (except Global environment) are reverted to the state
 from before the beginning of the module, and:
 
-a) the objects (again, since last Declaremods.start_module or
+1. the objects (again, since last Declaremods.start_module or
    Library.start_library) are classified using the classify_function.
    To simplify consider only those who returned Substitute _ or Keep _.
 
-b) If the module is not a functor, the subst_function for each object of
+2. If the module is not a functor, the subst_function for each object of
    the first group is called with the substitution 
    [MPself "<Datatypes#1>" |-> MPfile "Coq.Init.Datatypes"].
    Then the load_function is called for substituted objects and the
    "keep" object. 
    (If the module is a library the substitution is done at reloading).
 
-c) The objects which returned substitute are stored in the modtab
+3. The objects which returned substitute are stored in the modtab
    together with the self ident of the module, and functor argument
    names if the module was a functor.
 
@@ -744,9 +1177,9 @@ c) The objects which returned substitute are stored in the modtab
    is evaluated
 
 
-The difference between "substitute" and "keep" objects
-========================================================
-i) The "keep" objects can _only_ reference other objects by section_paths
+#### The difference between "substitute" and "keep" objects
+
+1. The "keep" objects can _only_ reference other objects by section_paths
 and qualids. They do not need the substitution function.
 
 They will work after end_module (or reloading a compiled library),
@@ -758,7 +1191,7 @@ These would typically be grammar rules, pretty printing rules etc.
 
 
 
-ii) The "substitute" objects can _only_ reference objects by
+2. The "substitute" objects can _only_ reference objects by
 kernel_names. They must have a valid subst_function. 
 
 They will work after end_module _and_ after Module Z:=N or 
@@ -767,17 +1200,18 @@ Module Z:=F(M).
 
 
 Other kinds of objects:
-iii) "Dispose" - objects which do not survive end_module
+
+3. "Dispose" - objects which do not survive end_module
      As a consequence, objects which reference other objects sometimes
      by kernel_names and sometimes by section_path must be of this kind...
 
-iv) "Anticipate" - objects which must be treated individually by
+4. "Anticipate" - objects which must be treated individually by
     end_module (typically "REQUIRE" objects)
 
 
 
-Writing subst_thing functions
-=============================
+#### Writing subst_thing functions
+
 The subst_thing shoud not copy the thing if it hasn't actually
 changed. There are some cool emacs macros in dev/objects.el 
 to help writing subst functions this way quickly and without errors.
@@ -792,15 +1226,13 @@ They are all (apart from constr, for now) written in the non-copying
 way.
 
 
-Nametab
-=======
+#### Nametab
 
 Nametab has been made more uniform. For every kind of thing there is
 only one "push" function and one "locate" function. 
 
 
-Lib
-===
+#### Lib
 
 library_segment is now a list of object_name * library_item, where
 object_name = section_path * kernel_name (see above)
@@ -808,20 +1240,19 @@ object_name = section_path * kernel_name (see above)
 New items have been added for open modules and module types
 
 
-Declaremods
-==========
+#### Declaremods
+
 Functions to declare interactive and noninteractive modules and module
 types.
 
 
-Library
-=======
+#### Library
+
 Uses Declaremods to actually communicate with Global and to register
 objects.
 
 
-OTHER CHANGES
-=============
+### Other changes
 
 Internal representation of tactics bindings has changed (see type
 Rawterm.substitution).
@@ -838,258 +1269,48 @@ New parsing model for tactics and vernacular commands
     TACTIC EXTEND ... END  to be used in ML files
 
 New organisation of THENS:
-tclTHENS tac tacs : tacs is now an array
-tclTHENSFIRSTn tac1 tacs tac2 :
+
+- tclTHENS tac tacs : tacs is now an array
+- tclTHENSFIRSTn tac1 tacs tac2 :
   apply tac1 then, apply the array tacs on the first n subgoals and
   tac2 on the remaining subgoals (previously tclTHENST)
-tclTHENSLASTn tac1 tac2 tacs :
+- tclTHENSLASTn tac1 tac2 tacs :
   apply tac1 then, apply tac2 on the first subgoals and apply the array
   tacs on the last n subgoals
-tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI)
-tclTHENLASTn tac1 tacs  = tclTHENSLASTn tac1 tclIDTAC tacs
-tclTHENFIRST tac1 tac2  = tclTHENFIRSTn tac1 [|tac2|]
-tclTHENLAST tac1 tac2   = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL)
-tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number")
-tclTHENSV same as tclTHENS but with an array
-tclTHENSi : no longer available
+- tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI)
+- tclTHENLASTn tac1 tacs  = tclTHENSLASTn tac1 tclIDTAC tacs
+- tclTHENFIRST tac1 tac2  = tclTHENFIRSTn tac1 [|tac2|]
+- tclTHENLAST tac1 tac2   = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL)
+- tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number")
+- tclTHENSV same as tclTHENS but with an array
+- tclTHENSi : no longer available
 
 Proof_type: subproof field in type proof_tree glued with the ref field
 
 Tacmach: no more echo from functions of module Refiner
 
 Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v.
+
 Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
   VERNAC COMMAND EXTEND macros
+
 File syntax/PPTactic.v moved to parsing/pptactic.ml
+
 Tactics about False and not now in tactics/contradiction.ml
+
 Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v)
+
 File tacinterp.ml moved from proofs to directory tactics
 
 
-==========================================
-= MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 =
-==========================================
+## Changes between Coq 7.1 and Coq 7.2
 
 The core of Coq (kernel) has meen minimized with the following effects:
 
-kernel/term.ml      split into kernel/term.ml,      pretyping/termops.ml
-kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml
-kernel/names.ml     split into kernel/names.ml,     library/nameops.ml
-kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml
+- kernel/term.ml      split into kernel/term.ml,      pretyping/termops.ml
+- kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml
+- kernel/names.ml     split into kernel/names.ml,     library/nameops.ml
+- kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml
 
 the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors,
 e.g. IsRel is now Rel, IsMutCase is now Case, etc.
-
-
-=======================================================
-= PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0 =
-=======================================================
-
-Changements d'organisation / modules :
---------------------------------------
-
-  Std, More_util		-> lib/util.ml
-
-  Names				-> kernel/names.ml et kernel/sign.ml
-    (les parties noms et signatures ont été séparées)
-
-  Avm,Mavm,Fmavm,Mhm  ->  utiliser plutôt Map (et freeze alors gratuit)
-  Mhb                 ->  Bij
-
-  Generic est intégré à Term (et un petit peu à Closure)
-
-Changements dans les types de données :
----------------------------------------
-  dans Generic: free_rels : constr -> int Listset.t
-                  devient : constr -> Intset.t
-
-  type_judgement ->  typed_type
-  environment    ->  context
-  context        ->  typed_type signature
-
-
-ATTENTION:
-----------
-
-  Il y a maintenant d'autres exceptions que UserError (TypeError,
-  RefinerError, etc.)
-
-  Il ne faut donc plus se contenter (pour rattraper) de faire
-  
-		try . .. with UserError _ -> ...
-
-  mais écrire à la place
- 
-                try ... with e when Logic.catchable_exception e -> ...
-
-
-Changements dans les fonctions :
---------------------------------
-
-	Vectops.
-	  it_vect          ->  Array.fold_left
-	  vect_it          ->  Array.fold_right
-	  exists_vect      ->  Util.array_exists
-	  for_all2eq_vect  ->  Util.array_for_all2
-	  tabulate_vect    ->  Array.init
-	  hd_vect          ->  Util.array_hd
-	  tl_vect          ->  Util.array_tl
-	  last_vect        ->  Util.array_last
-	  it_vect_from     ->  array_fold_left_from
-	  vect_it_from     ->  array_fold_right_from
-	  app_tl_vect	   ->  array_app_tl
-	  cons_vect	   ->  array_cons
-	  map_i_vect	   ->  Array.mapi
-	  map2_vect	   ->  array_map2
-	  list_of_tl_vect  ->  array_list_of_tl
-
-        Names
-          sign_it        -> fold_var_context (se fait sur env maintenant)
-	  it_sign        -> fold_var_context_reverse (sur env maintenant)
-
-        Generic
-	  noccur_bet     -> noccur_between
-          substn_many    -> substnl
-
-	Std 
-	  comp           ->  Util.compose
-	  rev_append	 ->  List.rev_append
-
-	Termenv
-	  mind_specif_of_mind  -> Global.lookup_mind_specif
-                ou Environ.lookup_mind_specif si on a un env sous la main
-	  mis_arity      ->  instantiate_arity
-	  mis_lc	 ->  instantiate_lc	
-
-	Ex-Environ	 
-	  mind_of_path      -> Global.lookup_mind
-
-	Printer
-	  gentermpr	->   gen_pr_term
-          term0	        ->   prterm_env	
-          pr_sign       ->   pr_var_context
-	  pr_context_opt -> pr_context_of
-          pr_ne_env      -> pr_ne_context_of
-
-	Typing, Machops
-	  type_of_type     ->  judge_of_type
-	  fcn_proposition  ->  judge_of_prop_contents
-	  safe_fmachine    ->  safe_infer
-
-	Reduction, Clenv
-          whd_betadeltat      -> whd_betaevar
-          whd_betadeltatiota  -> whd_betaiotaevar
-          find_mrectype       -> Inductive.find_mrectype
-          find_minductype     -> Inductive.find_inductive
-          find_mcoinductype   -> Inductive.find_coinductive
-
-        Astterm
-          constr_of_com_casted -> interp_casted_constr
-          constr_of_com_sort   -> interp_type
-          constr_of_com        -> interp_constr
-          rawconstr_of_com     -> interp_rawconstr
-          type_of_com          -> type_judgement_of_rawconstr
-	  judgement_of_com     -> judgement_of_rawconstr
-
-        Termast
-          bdize                -> ast_of_constr
-
-        Tacmach
-          pf_constr_of_com_sort -> pf_interp_type
-          pf_constr_of_com      -> pf_interp_constr
-	  pf_get_hyp            -> pf_get_hyp_typ
-          pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant)
-
-        Pattern
-	  raw_sopattern_of_compattern -> Astterm.interp_constrpattern
-	  somatch               -> is_matching
-          dest_somatch          -> matches
-
-        Tacticals
-	  matches               -> gl_is_matching
-          dest_match            -> gl_matches
-	  suff                  -> utiliser sort_of_goal
-          lookup_eliminator     -> utiliser sort_of_goal pour le dernier arg
-
-        Divers
-          initial_sign     -> var_context
-
-        Sign
-          ids_of_sign      -> ids_of_var_context (or Environ.ids_of_context)
-          empty_sign       -> empty_var_context
-
-        Pfedit
-	  list_proofs      -> get_all_proof_names
-          get_proof        -> get_current_proof_name
-          abort_goal       -> abort_proof
-          abort_goals      -> abort_all_proofs
-          abort_cur_goal   -> abort_current_proof
-          get_evmap_sign   -> get_goal_context/get_current_goal_context
-          unset_undo       -> reset_undo
-
-        Proof_trees
-          mkGOAL           -> mk_goal
-
-        Declare
-  	  machine_constant ->   declare_constant (+ modifs)
-
-	ex-Trad, maintenant Pretyping
-          inh_cast_rel        -> Coercion.inh_conv_coerce_to
-          inh_conv_coerce_to  -> Coercion.inh_conv_coerce_to_fail
-	  ise_resolve1        -> understand, understand_type
-	  ise_resolve         -> understand_judgment, understand_type_judgment
-
-        ex-Tradevar, maintenant Evarutil
-          mt_tycon            -> empty_tycon
-
-        Recordops
-          struc_info          -> find_structure
-
-Changements dans les inductifs
-------------------------------
-Nouveaux types "constructor" et "inductive" dans Term
-La plupart des fonctions de typage des inductives prennent maintenant
-un inductive au lieu d'un oonstr comme argument. Les seules fonctions
-à traduire un constr en inductive sont les find_rectype and co.
-
-Changements dans les grammaires
--------------------------------
-
- . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex
-
- . attention : LIDENT -> IDENT  (les identificateurs n'ont pas de
-                                 casse particulière dans Coq)
-
- . Le mot "command" est remplacé par "constr" dans les noms de
- fichiers, noms de modules et non-terminaux relatifs au parsing des
- termes; aussi les changements suivants "COMMAND"/"CONSTR" dans
- g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml*
-
- . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n
-   passent en minuscule Identifier, Constr, ...
- 
- . Plusieurs parsers ont changé de format (ex: sortarg)
-
-Changements dans le pretty-printing
------------------------------------
-
- . Découplage de la traduction de constr -> rawconstr (dans detyping)
-    et de rawconstr -> ast (dans termast)
- . Déplacement des options d'affichage de printer vers termast
- . Déplacement des réaiguillage d'univers du pp de printer vers esyntax
-
-	
-Changements divers
-------------------
-
- . il n'y a plus de script coqtop => coqtop et coqtop.byte sont
-   directement le résultat du link du code
-   => debuggage et profiling directs
-
- . il n'y a plus d'installation locale dans bin/$ARCH
- 
- . #use "include.ml"  =>  #use "include"
-   go()               =>  loop()
-
- . il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
-   de temps
diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd
index f2314e22..cc33efd4 100644
--- a/dev/doc/cic.dtd
+++ b/dev/doc/cic.dtd
@@ -125,7 +125,7 @@
           id     ID     #REQUIRED
           sort   %sort; #REQUIRED>
 
-<!-- The substitutions are ordered by increasing DeBrujin  -->
+<!-- The substitutions are ordered by increasing de Bruijn  -->
 <!-- index. An empty substitution means that that index is -->
 <!-- not accessible.                                       -->
 <!ELEMENT META (substitution*)>
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index 00e7f5c5..b3d49b7e 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -14,11 +14,6 @@ parsing
 tactics
 toplevel
 
-highparsing :
-
- Files in parsing/ that cannot be linked too early.
- Contains the grammar rules g_*.ml4
-
 Special components
 ------------------
 
@@ -30,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/debugging.md b/dev/doc/debugging.md
new file mode 100644
index 00000000..14a1cc69
--- /dev/null
+++ b/dev/doc/debugging.md
@@ -0,0 +1,106 @@
+Debugging from Coq toplevel using Caml trace mechanism
+======================================================
+
+  1. Launch bytecode version of Coq (coqtop.byte)
+  2. Access Ocaml toplevel using vernacular command 'Drop.'
+  3. Install load paths and pretty printers for terms, idents, ... using
+     Ocaml command '#use "base_include";;' (use '#use "include";;' for 
+     installing the advanced term pretty printers)
+  4. Use #trace to tell which function(s) to trace
+  5. Go back to Coq toplevel with 'go();;'
+  6. Test your Coq command and observe the result of tracing your functions
+  7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;'
+
+  You can avoid typing #use "include" (or "base_include") after Drop
+  by adding the following lines in your $HOME/.ocamlinit :
+
+   if Filename.basename Sys.argv.(0) = "coqtop.byte"
+   then ignore (Toploop.use_silently Format.std_formatter "include")
+
+  Hints: To remove high-level pretty-printing features (coercions,
+  notations, ...), use "Set Printing All". It will affect the #trace
+  printers too.
+
+
+Debugging with ocamldebug from Emacs
+====================================
+
+   Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\
+   Coq must be configured with `-local` (`./configure -local`) and the
+   byte-code version of `coqtop` must have been generated with `make byte`.
+
+   1. M-x camldebug
+   2. give the binary name bin/coqtop.byte
+   3. give ../dev/ocamldebug-coq
+   4. source db  (to get pretty-printers)
+   5. add breakpoints with C-x C-a C-b from the buffer displaying the ocaml
+      source
+   6. get more help from ocamldebug manual
+         run
+	 step
+         back
+         start
+	 next
+	 last
+	 print x (abbreviated into p x)
+	 ...
+   7. some hints: 
+
+   - To debug a failure/error/anomaly, add a breakpoint in
+     `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com
+     with ..." block, then go "back" a few steps to find where the
+     failure/error/anomaly has been raised
+   - Alternatively, for an error or an anomaly, add breakpoints in the middle  
+     of each of error* functions or anomaly* functions in lib/util.ml
+   - If "source db" fails, do a "make printers" and try again (it should build
+     top_printers.cmo and the core cma files).
+   - If you build Coq with an OCaml version earlier than 4.06, and have the 
+     OCAMLRUNPARAM environment variable set, Coq may hang on startup when run 
+     from the debugger. If this happens, unset the variable, re-start Emacs, and 
+     run the debugger again.
+
+Debugging with ocamldebug from the command line
+===============================================
+
+In the `coq` directory:
+1. (on Cygwin/Windows) Pass the `-no-custom` option to the `configure` script before building Coq.
+2. Run `make` (to compile the .v files)
+3. Run `make byte`
+4. (on Cygwin/Windows) Add the full pathname of the directory `.../kernel/byterun` to your bash PATH.
+   Alternatively, copy the file `kernel/byterun/dllcoqrun.dll` to a directory that is in the PATH.  (The
+   CAML_LD_LIBRARY_PATH mechanism described at the end of INSTALL isn't working.)
+5. Run `dev/ocamldebug-coq bin/coqtop.byte`  (on Cygwin/Windows, use `... bin/coqtop.byte.exe`)
+6. Enter `source db` to load printers
+7. Enter `set arguments -coqlib .` so Coq can find plugins, theories, etc.
+8. See the ocamldebug manual for more information.  A few points:
+   - use `break @ Printer 501` to set a breakpoint on line 501 in the Printer module (printer.ml).
+     `break` can be abbreviated as `b`.
+   - `backtrace` or `bt` to see the call stack
+   - `step` or `s` goes into called functions; `next` or `n` skips over them
+   - `list` or `li` shows the code just before and after the current stack frame
+   - `print <var>` or `p <var>` to see the value of a variable
+Note that `make byte` doesn't recompile .v files.  `make` recompiles all of them if there
+are changes in any .ml file--safer but much slower.
+
+Global gprof-based profiling
+============================
+
+   Coq must be configured with option -profile
+
+   1. Run native Coq which must end normally (use Quit or option -batch)
+   2. gprof ./coqtop gmon.out
+
+Per function profiling
+======================
+
+   To profile function foo in file bar.ml, add the following lines, just
+   after the definition of the function:
+
+     let fookey = CProfile.declare_profile "foo";;
+     let foo a b c = CProfile.profile3 fookey foo a b c;;
+
+   where foo is assumed to have three arguments (adapt using
+   Profile.profile1, Profile. profile2, etc).
+
+   This has the effect to cumulate the time passed in foo under a
+   line of name "foo" which is displayed at the time coqtop exits.
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
deleted file mode 100644
index f0df2fc3..00000000
--- a/dev/doc/debugging.txt
+++ /dev/null
@@ -1,78 +0,0 @@
-Debugging from Coq toplevel using Caml trace mechanism
-======================================================
-
-  1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte)
-  2. Access Ocaml toplevel using vernacular command 'Drop.'
-  3. Install load paths and pretty printers for terms, idents, ... using
-     Ocaml command '#use "base_include";;' (use '#use "include";;' for 
-     installing the advanced term pretty printers)
-  4. Use #trace to tell which function(s) to trace
-  5. Go back to Coq toplevel with 'go();;'
-  6. Test your Coq command and observe the result of tracing your functions
-  7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;'
-
-  You can avoid typing #use "include" (or "base_include") after Drop
-  by adding the following lines in your $HOME/.ocamlinit :
-
-   if Filename.basename Sys.argv.(0) = "coqtop.byte"
-   then ignore (Toploop.use_silently Format.std_formatter "include")
-
-  Hints: To remove high-level pretty-printing features (coercions,
-  notations, ...), use "Set Printing All". It will affect the #trace
-  printers too.
-
-
-Debugging from Caml debugger
-============================
-
-   Needs tuareg mode in Emacs
-   Coq must be configured with -debug and -local (./configure -debug -local)
-
-   1. M-x camldebug
-   2. give the binary name bin/coqtop.byte
-   3. give ../dev/ocamldebug-coq
-   4. source db  (to get pretty-printers)
-   5. add breakpoints with C-x C-a C-b from the buffer displaying the ocaml
-      source
-   6. get more help from ocamldebug manual
-         run
-	 step
-         back
-         start
-	 next
-	 last
-	 print x (abbreviated into p x)
-	 ...
-   7. some hints: 
-
-   - To debug a failure/error/anomaly, add a breakpoint in
-     Vernac.vernac_com at the with clause of the "try ... interp com
-     with ..." block, then go "back" a few steps to find where the
-     failure/error/anomaly has been raised
-   - Alternatively, for an error or an anomaly, add breakpoints in the middle  
-     of each of error* functions or anomaly* functions in lib/util.ml
-   - If "source db" fails, recompile printers.cma with
-     "make dev/printers.cma" and try again
-
-Global gprof-based profiling
-============================
-
-   Coq must be configured with option -profile
-
-   1. Run native Coq which must end normally (use Quit or option -batch)
-   2. gprof ./coqtop gmon.out
-
-Per function profiling
-======================
-
-   1. To profile function foo in file bar.ml, add the following lines, just
-      after the definition of the function:
-
-     let fookey = Profile.declare_profile "foo";;
-     let foo a b c = Profile.profile3 fookey foo a b c;;
-
-     where foo is assumed to have three arguments (adapt using
-     Profile.profile1, Profile. profile2, etc).
-
-     This has the effect to cumulate the time passed in foo under a
-     line of name "foo" which is displayed at the time coqtop exits.
diff --git a/dev/doc/econstr.md b/dev/doc/econstr.md
new file mode 100644
index 00000000..bb17e8fb
--- /dev/null
+++ b/dev/doc/econstr.md
@@ -0,0 +1,129 @@
+# Evar-insensitive terms (EConstr)
+
+Evar-insensitive terms were introduced in 8.7, following
+[CEP #10](https://github.com/coq/ceps/blob/master/text/010-econstr.md). We will
+not recap the motivations in this document and rather summarize the code changes
+to perform.
+
+## Overview
+
+The essential datastructures are defined in
+[the `EConstr` module](/engine/eConstr.mli) module. It defines
+the tactic counterparts of kernel data structures such as terms
+(`EConstr.constr`), universes (`EConstr.ESorts.t`) and contexts
+(`EConstr.*_context`).
+
+The main difference with kernel-side types is that observing them requires
+an evar-map at hand in order to normalize evars on the fly. The basic primitive
+to observe an `EConstr.t` is the following function:
+```
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
+(** Same as {!Constr.kind} except that it expands evars and normalizes
+    universes on the fly. *)
+```
+
+Essentially, each time it sees an evar which happens to be defined in the
+provided evar-map, it replaces it with the corresponding body and carries on.
+
+Due to universe unification occuring at the tactic level, the same goes for
+universe instances and sorts. See the `ESort` and `EInstance` modules in
+`EConstr`.
+
+This normalization is critical for the soundness of tactics. Before EConstr, a
+lot of bugs were lurking in the code base, a few still are (most notably in
+meta-based unification) and failure to respect the guidelines thereafter may
+result in nasal demons.
+
+## Transition path
+
+### Types
+
+As a rule of thumb, all functions living at the tactic level should manipulate
+`EConstr.t` instead of `Constr.t`, and similarly for the other data structures.
+
+To ease the transition, the `EConstr` module defines a handful of aliases to
+shadow the type names from the kernel.
+
+It is recommended to perform the following replacement in headers.
+```ocaml
+(** Kernel types. You may remove the two following opens if you want. Beware
+    that [kind_of_term] needs to be in scope if you use [EConstr.kind] so that
+    you may still need to open one of the two. *)
+open Term
+open Constr
+(** Tactic types. Open this after to shadow kernel types. *)
+open EConstr
+```
+
+Note that the `EConstr` module also redefines a `Vars` submodule.
+
+### Evar-map-passing
+
+All functions deconstructing an econstr need to take an evar-map as a parameter.
+Therefore, you need to pass one as an argument virtually everywhere.
+
+In the Coq source code, it is recommended to take the evar-map as a first
+argument called `sigma`, except if the function also takes an environment in
+which case it is passed second. Namely, the two typical instances are:
+```ocaml
+let foo sigma c = mycode
+val foo : Evd.evar_map -> EConstr.t -> Foo.t
+
+let bar env sigma c = mycode
+val bar : Environ.env -> Evd.evar_map -> EConstr.t -> Bar.t
+```
+
+The EConstr API makes the code much more sensitive to evar-maps, because a
+lot of now useless normalizations were removed. Thus one should be cautious of
+**not** dropping the evar-map when it has been updated, and should rather stick
+to a strict state-passing discipline. Unsound primitives like
+`Typing.unsafe_type_of` are also a known source of problems, so you should
+replace them with the corresponding evar-map-returning function and thread it
+properly.
+
+### Functions
+
+Many functions from `Constr` and `Term` are redefined to work on econstr in
+the `EConstr` module, so that it is often enough to perform the `open` as
+described above to replace them. Their type may differ though, because they now
+need access to an evar-map. A lot of econstr-manipulating functions are also
+defined in [`Termops`](/engine/termops.mli).
+
+Functions manipulating tactic terms and kernel terms share the same name if they
+are the equivalent one of the other. Do not hesitate to grep Coq mli files to
+find the equivalent of a function you want to port if it is neither in `EConstr`
+nor in `Termops` (this should be very rare).
+
+### Conversion
+
+Sometimes you do not have any other choice than calling kernel-side functions
+on terms, and conversely to turn a kernel term into a tactic term.
+
+There are two functions to do so.
+* `EConstr.of_constr` turns kernel terms into tactic terms. It is currently
+the physical identity, and thus O(1), but this may change in the future.
+* `EConstr.to_constr` turns tactic terms into kernel terms. It performs a
+full-blown normalization of the given term, which is O(n) and potentially
+costly.
+
+For performance reasons, avoiding to jump back and forth between kernel and
+tactic terms is recommended.
+
+There are also a few unsafe conversion functions that take advantage of the
+fact that `EConstr.t` is internally the same as `Constr.t`. Namely,
+`EConstr.Unsafe.to_constr` is the physical identity. It should **not** be used
+in typical code and is instead provided for efficiency **when you know what you
+are doing**. Either use it to reimplement low-level functions that happen to
+be insensitive externally, or use it to provide backward compatibility with
+broken code that relies on evar-sensitivity. **Do not use it because it is
+easier than stuffing evar-maps everywhere.** You've been warned.
+
+## Notes
+
+The EConstr branch fixed a lot of eisenbugs linked to lack of normalization
+everywhere, most notably in unification. It may also have introduced a few, so
+if you see a change in behaviour *that looks like a bug*, please report it.
+Obviously, unification is not specified, so it's hard to tell apart, but still.
+
+Efficiency has been affected as well. We now pay an overhead when observing a
+term, but at the same time a lot of costly upfront normalizations were removed.
diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex
index 34916494..337b9226 100644
--- a/dev/doc/naming-conventions.tex
+++ b/dev/doc/naming-conventions.tex
@@ -267,7 +267,7 @@ If the conclusion is in the other way than listed below, add suffix
 {forall x y:D, op (op' x y) = op' x (op y)}
 
 \itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent}
-{forall x:D, op x n = x}
+{forall x:D, op x x = x}
 
 \itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent}
 {forall x:D, op (op x) = op x}
diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion.v
index a81f170c..a81f170c 100644
--- a/dev/doc/notes-on-conversion
+++ b/dev/doc/notes-on-conversion.v
diff --git a/dev/doc/primproj.md b/dev/doc/primproj.md
new file mode 100644
index 00000000..ea76aeea
--- /dev/null
+++ b/dev/doc/primproj.md
@@ -0,0 +1,41 @@
+Primitive Projections
+---------------------
+
+    | Proj of Projection.t * constr
+
+Projections are always applied to a term, which must be of a record
+type (i.e. reducible to an inductive type `I params`). Type-checking,
+reduction and conversion are fast (not as fast as they could be yet)
+because we don't keep parameters around. As you can see, it's
+currently a `constant` that is used here to refer to the projection,
+that will change to an abstract `projection` type in the future.
+Basically a projection constant records which inductive it is a
+projection for, the number of params and the actual position in the
+constructor that must be projected. For compatibility reason, we also
+define an eta-expanded form (accessible from user syntax `@f`). The
+constant_entry of a projection has both informations. Declaring a
+record (under `Set Primitive Projections`) will generate such
+definitions. The API to declare them is not stable at the moment, but
+the inductive type declaration also knows about the projections, i.e.
+a record inductive type decl contains an array of terms representing
+the projections. This is used to implement eta-conversion for record
+types (with at least one field and having all projections definable).
+The canonical value being `Build_R (pn x) ... (pn x)`. Unification and
+conversion work up to this eta rule. The records can also be universe
+polymorphic of course, and we don't need to keep track of the universe
+instance for the projections either. Projections are reduced _eagerly_
+everywhere, and introduce a new `Zproj` constructor in the abstract
+machines that obeys both the delta (for the constant opacity) and iota
+laws (for the actual reduction). Refolding works as well (afaict), but
+there is a slight hack there related to universes (not projections).
+
+For the ML programmer, the biggest change is that pattern-matchings on
+kind_of_term require an additional case, that is handled usually
+exactly like an `App (Const p) arg`.
+
+There are slight hacks related to hints is well, to use the primitive
+projection form of f when one does `Hint Resolve f`. Usually hint
+resolve will typecheck the term, resulting in a partially applied
+projection (disallowed), so we allow it to take
+`constr_or_global_reference` arguments instead and special-case on
+projections. Other tactic extensions might need similar treatment.
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 9d2ebf0d..b5dd8445 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux.
 
 In Coq source folder:
 
-opam switch 4.02.1+fp
+opam switch 4.02.3+fp
 ./configure -local -debug
 make
 perf record -g bin/coqtop -compile file.v
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
new file mode 100644
index 00000000..8f96ac22
--- /dev/null
+++ b/dev/doc/proof-engine.md
@@ -0,0 +1,133 @@
+Tutorial on the new proof engine for ML tactic writers
+======================================================
+
+Starting from Coq 8.5, a new proof engine has been introduced, replacing the old
+meta-based engine which had a lot of drawbacks, ranging from expressivity to
+soundness, the major one being that the type of tactics was transparent. This
+was pervasively abused and made virtually impossible to tweak the implementation
+of the engine.
+
+The old engine is deprecated and is slowly getting removed from the source code.
+
+The new engine relies on a monadic API defined in the `Proofview` module. Helper
+functions and higher-level operations are defined in the `Tacmach` and
+`Tacticals` modules, and end-user tactics are defined amongst other in the
+`Tactics` module.
+
+At the root of the engine is a representation of proofs as partial terms that
+can contain typed holes, called evars, short for *existential variable*. An evar
+is essentially defined by its context and return type, that we will write
+`?e : [Γ ⊢ _ : A]`. An evar `?e` must be applied to a substitution `σ` of type
+`Γ` (i.e. a list of terms) to produce a term of type `A`, which is done by
+applying `EConstr.mkEvar`, and which we will write `?e{σ}`.
+
+The engine monad features a notion of global state called `evar_map`, defined in
+the `Evd` module, which is the structure containing the incremental refinement
+of evars. `Evd` is a low-level API and its use is discouraged in favour of the
+`Evarutil` module which provides more abstract primitives.
+
+In addition to this state, the monad also features a goal state, that is
+an ordered list of current holes to be filled. While these holes are referred
+to as goals at a high-enough level, they are actually no more than evars. The
+API provided to deal with these holes can be found in the `Proofview.Goal`
+module. Tactics are naturally operating on several goals at once, so that it is
+usual to use the `Proofview.Goal.enter` function and its variants to dispatch a
+tactic to each of the goals under focus.
+
+Primitive tactics by term refining
+-------------------------------------
+
+A typical low-level tactic will be defined by plugging partial terms in the
+goal holes thanks to the `Refine` module, and in particular to the
+`Refine.refine` primitive.
+
+```ocaml
+val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
+(** In [refine typecheck t], [t] is a term with holes under some
+    [evar_map] context. The term [t] is used as a partial solution
+    for the current goal (refine is a goal-dependent tactic), the
+    new holes created by [t] become the new subgoals. Exceptions
+    raised during the interpretation of [t] are caught and result in
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
+```
+
+In a first approximation, we can think of `'a Sigma.run` as
+`evar_map -> 'a * evar_map`. What the function does is first evaluate the
+`Constr.t Sigma.run` argument in the current proof state, and then use the
+resulting term as a filler for the proof under focus. All evars that have been
+created by the invocation of this thunk are then turned into new goals added in
+the order of their creation.
+
+To see how we can use it, let us have a look at an idealized example, the `cut`
+tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]`
+with a term `let x : X := ?e2{Γ} in ?e1{Γ} x` where `x` is a fresh variable and
+`?e1 : [Γ ⊢ _ : X -> A]` and `?e2 : [Γ ⊢ _ : X]`. The current goal is solved and
+two new holes `[e1, e2]` are added to the goal state in this order.
+
+```ocaml
+let cut c =
+  let open Sigma in
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+    (** In this block, we focus on one goal at a time indicated by gl *)
+    let env = Proofview.Goal.env gl in
+    (** Get the context of the goal, essentially [Γ] *)
+    let concl = Proofview.Goal.concl gl in
+    (** Get the conclusion [A] of the goal *)
+    let hyps = Tacmach.New.pf_ids_of_hyps gl in
+    (** List of hypotheses from the context of the goal *)
+    let id = Namegen.next_name_away Anonymous hyps in
+    (** Generate a fresh identifier *)
+    let t = mkArrow c (Vars.lift 1 concl) in
+    (** Build [X -> A]. Note the lifting of [A] due to being on the right hand
+        side of the arrow. *)
+    Refine.refine { run = begin fun sigma ->
+      (** All evars generated by this block will be added as goals *)
+      let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in
+      (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the
+          term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity
+          substitution for [Γ] is extracted from the [env] argument, so that
+          one must be careful to pass the correct context here in order for the
+          resulting term to be well-typed. The [p] return value is a proof term
+          used to enforce sigma monotonicity. *)
+      let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in
+      (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return
+          [x := Γ ⊢ ?e2{Γ} : X]. *)
+      let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in
+      (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *)
+      Sigma (r, sigma, p +> q)
+      (** Fills the current hole with [r]. The [p +> q] thingy ensures
+          monotonicity of sigma. *)
+    end }
+  end }
+```
+
+The `Evarutil.new_evar` function is the preferred way to generate evars in
+tactics. It returns a ready-to-use term, so that one does not have to call
+the `mkEvar` primitive. There are lower-level variants whose use is dedicated to
+special use cases, *e.g.* whenever one wants a non-identity substitution. One
+should take care to call it with the proper `env` argument so that the evar
+and term it generates make sense in the context they will be plugged in.
+
+For the sake of completeness, the old engine was relying on the `Tacmach.refine`
+function to provide a similar feature. Nonetheless, it was using untyped metas
+instead of evars, so that it had to mangle the argument term to actually produce
+the term that would be put into the hole. For instance, to work around the
+untypedness, some metas had to be coerced with a cast to enforce their type,
+otherwise leading to runtime errors. This was working for very simple
+instances, but was unreliable for everything else.
+
+High-level composition of tactics
+------------------------------------
+
+It is possible to combine low-level refinement tactics to create more powerful
+abstractions. While it was the standard way of doing things in the old engine
+to overcome its technical limitations (namely that one was forced to go through
+a limited set of derivation rules), it is recommended to generate proofs as
+much as possible by refining in ML tactics when it is possible and easy enough.
+Indeed, this prevents dependence on fragile constructions such as unification.
+
+Obviously, it does not forbid the use of tacticals to mimick what one would do
+in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple
+semantics. A list of such tacticals can be found in the `Tacticals` module. Most
+of them are a porting of the tacticals from the old engine to the new one, so
+that if they share the same name they are expected to have the same semantics.
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
index 1b016a4e..c48c2d5d 100644
--- a/dev/doc/setup.txt
+++ b/dev/doc/setup.txt
@@ -12,7 +12,7 @@ How to compile Coq
 
 Getting build dependencies:
 
-  sudo apt-get install make opam git mercurial darcs
+  sudo apt-get install make opam git
   opam init --comp 4.02.3
   # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files.
   
@@ -41,17 +41,15 @@ Building coqtop:
   cd ~/git/coq
   git checkout trunk
   make distclean
-  ./configure -annotate -with-doc no -local -debug -usecamlp5
+  ./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
-
-The "-debug" option is essential if one wants to use ocamldebug with the coqtop binary.
-
-Then check if
+Once the compilation is over check if
 - bin/coqtop
 - bin/coqide
 behave as expected.
@@ -60,30 +58,12 @@ behave as expected.
 A note about rlwrap
 -------------------
 
-Running "coqtop" under "rlwrap" is possible, but there is a catch. If you try:
-
-  cd ~/git/coq
-  rlwrap bin/coqtop
-
-you will get an error:
+When using "rlwrap coqtop" make sure the version of rlwrap is at least
+0.42, otherwise you will get
 
   rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory
 
-This is a known issue:
-
-  https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=779692
-
-It was fixed upstream in version 0.42, and in a Debian package that, at the time of writing, is not part of Debian stable/testing/sid archives but only of Debian experimental.
-
-  https://packages.debian.org/experimental/rlwrap
-
-The quick solution is to grab it from there, since it installs fine on Debian stable (jessie).
-
-  cd /tmp
-  wget  http://ftp.us.debian.org/debian/pool/main/r/rlwrap/rlwrap_0.42-1_amd64.deb
-  sudo dpkg -i rlwrap_0.42-1_amd64.deb
-
-After that, "rlwrap" works fine with "coqtop".
+If this happens either update or use an alternate readline wrapper like "ledit".
 
 
 How to install and configure Merlin (for Emacs)
@@ -281,7 +261,7 @@ You can load them by switching to the window holding the "ocamldebug" shell and
 Some of the functions were you might want to set a breakpoint and see what happens next
 ---------------------------------------------------------------------------------------
 
-- Coqtop.start : This function is called by the code produced by "coqmktop".
+- Coqtop.start : This function is the main entry point of coqtop.
 - Coqtop.parse_args : This function is responsible for parsing command-line arguments.
 - Coqloop.loop : This function implements the read-eval-print loop.
 - Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\
diff --git a/dev/doc/style.txt b/dev/doc/style.txt
index 27695a09..2ee3dadd 100644
--- a/dev/doc/style.txt
+++ b/dev/doc/style.txt
@@ -1,75 +1,142 @@
-
-<< L'uniformité du style est plus importante que le style lui-même. >>
-(Kernigan & Pike, The Practice of Programming)
-
-Mode Emacs
-==========
-   Tuareg, que l'on trouve ici :  http://www.prism.uvsq.fr/~acohen/tuareg/
-
-   avec le réglage suivant :     (setq tuareg-in-indent 2)
-
-Types récursifs et filtrages
-============================
-   Une barre de séparation y compris sur le premier constructeur
-
-type t =
-  | A 
-  | B of machin
-
-match expr with
-  | A -> ...
-  | B x -> ...
-
-Remarque : à partir de la 8.2 environ, la tendance est à utiliser le
-format suivant qui permet de limiter l'escalade d'indentation tout en
-produisant un aspect visuel intéressant de bloc :
-
-type t =
-| A 
-| B of machin
-
-match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = function
-| A -> ...
-| B x -> ...
-
-Le deuxième cas est obtenu sous tuareg avec les réglages
-
-  (setq tuareg-with-indent 0)
-  (setq tuareg-function-indent 0)
-  (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien 
-                                      /// pour les let mais pas pour les let-in
-
-Conditionnelles
-===============
-  if condition then
-    premier-cas
-  else
-    deuxieme-cas
-
-  Si effets de bord dans les branches, utilisez begin ... end et non des
-  parenthèses i.e.
-
-  if condition then begin
-    instr1;
-    instr2
-  end else begin
-    instr3;
-    instr4
-  end
-    
-  Si la première branche lève une exception, évitez le else i.e.
-
-    if condition then                     if condition then error "machin";
-      error "machin"          ----->      suite
+<< Style uniformity is more important than style itself >>
+   (Kernigan & Pike, The Practice of Programming)
+
+OCaml Style:
+- Spacing and indentation
+  - indent your code (using tuareg default)
+  - no strong constraints in formatting "let in"; possible styles are:
+    "let x = ... in"
+    "let x =
+       ... in"
+    "let
+       x = ...
+     in"
+  - but: no extra indentation before a "in" coming on next line,
+    otherwise, it first shifts further and further on the right,
+    reducing the amount of space available; second, it is not robust to
+    insertion of a new "let"
+  - it is established usage to have space around "|" as in
+    "match c with
+     | [] | [a] -> ...
+     | a::b::l -> ..."
+  - in a one-line "match", it is preferred to have no "|" in front of
+    the first case (this saves spaces for the match to hold in the line)
+  - from about 8.2, the tendency is to use the following format which
+    limit excessive indentation while providing an interesting "block" aspect
+    type t =
+    | A 
+    | B of machin
+
+    let f expr = match expr with
+    | A -> ...
+    | B x -> ...
+
+    let f expr = function
+    | A -> ...
+    | B x -> ...
+  - add spaces around = and == (make the code "breaths")
+  - the common usage is to write "let x,y = ... in ..." rather than
+    "let (x,y) = ... in ..."
+  - parenthesizing with either "(" and ")" or with "begin" and "end" is
+    common practice
+  - preferred layout for conditionals:
+    if condition then
+      premier-cas
     else
-      suite
-
-  
+      deuxieme-cas
+  - in case of effects in branches, use "begin ... end" rather than
+    parentheses
+    if condition then begin
+      instr1;
+      instr2
+    end else begin
+      instr3;
+      instr4
+    end
+  - if the first branch raises an exception, avoid the "else", i.e.:
+    if condition then                     if condition then error "foo";
+      error "foo"          ----->         bar
+    else
+      bar
+  - it is the usage not to use ;; to end OCaml sentences (however,
+    inserting ";;" can be useful for debugging syntax errors crossing
+    the boundary of functions)
+  - relevant options in tuareg:
+    (setq tuareg-in-indent 2)
+    (setq tuareg-with-indent 0)
+    (setq tuareg-function-indent 0)
+    (setq tuareg-let-always-indent nil)
+
+- Coding methodology
+  - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C),
+    Out_of_memory, Stack_overflow, etc.
+    at least, use "try with e when Errors.noncritical e -> ..."
+    (to be detailed, Pierre L. ?)
+  - do not abuse of fancy combinators: sometimes what a "let rec" loop
+    does is more readable and simpler to grasp than what a "fold" does
+  - do not break abstractions: if an internal property is hidden
+    behind an interface, do no rely on it in code which uses this
+    interface (e.g. do not use List.map thinking it is left-to-right,
+    use map_left)
+  - in particular, do not use "=" on abstract types: there is no
+    reason a priori that it is the intended equality on this type; use the
+    "equal" function normally provided with the abstract type
+  - avoid polymorphically typed "=" whose implementation is not
+    optimized in OCaml and which has moreover no reason to be the
+    intended implementation of the equality when it comes to be
+    instantiated on a particular type (e.g. use List.mem_f,
+    List.assoc_f, rather than List.mem, List.assoc, etc, unless it is
+    absolutely clear that "=" will implement the intended equality, and
+    with the right complexity)
+  - any new general-purpose enough combinator on list should be put in
+    cList.ml, on type option in cOpt.ml, etc.
+  - unless of a good reason not to so, follow the style of the
+    surrounding code in the same file as much as possible,
+    the general guidelines are otherwise "let spacing breaths" (we
+    have large screen nowadays), "make your code easy to read and
+    to understand"
+  - document what is tricky, but do not overdocument, sometimes the
+    choice of names and the structuration of the code is a better
+    documentation than a long discourse; use of unicode in comments is
+    welcome if it can make comments more readable (then
+    "toggle-enable-multibyte-characters" can help when using the
+    debugger in emacs)
+  - all of initial "open File", or of small-scope File.(...), or
+    per-ident File.foo are common practices
+
+- Choice of variable names
+  - be consistent when naming from one function to another
+  - be consistent with the naming adopted in the functions from the
+    same file, or with the naming used elsewhere by similar functions
+  - use variable names which express meaning
+  - keep "cst" for constants and avoid it for constructors which is
+    otherwise a source of confusion
+  - for constructors, use "cstr" in type constructor (resp. "cstru" in
+    constructor puniverse); avoid "constr" for "constructor" which
+    could be think as the name of an arbitrary Constr.t
+  - for inductive types, use "ind" in the type inductive (resp "indu"
+    in inductive puniverse)
+  - for env, use "env"
+  - for evar_map, use "sigma", with tolerance into "evm" and "evd"
+  - for named_context or rel_context, use "ctxt" or "ctx" (or "sign")
+  - for formal/actual indices of inductive types: "realdecls", "realargs"
+  - for formal/actual parameters of inductive types: "paramdecls", "paramargs"
+  - for terms, use e.g. c, b, a, ...
+  - if a term is known to be a function: f, ...
+  - if a term is known to be a type: t, u, typ, ...
+  - for a declaration, use d or "decl"
+  - for errors, exceptions, use e
+
+- Common OCaml pitfalls
+  - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in
+    "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in
+    parentheses are needed around the "try" and the inner "match"
+  - even if stream are lazy, the Pp.(++) combinator is strict and
+    forces the evaluation of its arguments (use a "lazy" or a "fun () ->")
+    to make it lazy explicitly
+  - in "if ... then ... else ... ++ ...", the default parenthesizing
+    is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..."
+  - in "let myspecialfun = mygenericfun args", be sure that it does no
+    do side-effect; prefer otherwise "let mygenericfun arg =
+    mygenericfun args arg" to ensure that the function is evaluated at
+    runtime
diff --git a/dev/doc/univpoly.txt b/dev/doc/universes.md
index 6a69c579..c276603e 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/universes.md
@@ -1,44 +1,45 @@
-Notes on universe polymorphism and primitive projections, M. Sozeau
-===================================================================
+Notes on universe polymorphism
+------------------------------
 
-The new implementation of universe polymorphism and primitive
-projections introduces a few changes to the API of Coq. First and
-foremost, the term language changes, as global references now carry a
-universe level substitution:
+The implementation of universe polymorphism introduces a few changes
+to the API of Coq. First and foremost, the term language changes, as
+global references now carry a universe level substitution:
 
+~~~ocaml
 type 'a puniverses = 'a * Univ.Instance.t
 type pconstant = constant puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
 type constr = ...
-  | Const of puniversess
+  | Const of puniverses
   | Ind of pinductive
   | Constr of pconstructor
-  | Proj of constant * constr
-
+~~~
 
 Universes
-=========
+---------
 
-  Universe instances (an array of levels) gets substituted when
+Universe instances (an array of levels) gets substituted when
 unfolding definitions, are used to typecheck and are unified according
-to the rules in the ITP'14 paper on universe polymorphism in Coq.  
+to the rules in the ITP'14 paper on universe polymorphism in Coq.
 
+~~~ocaml
 type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *)
 type Instance.t = Level.t array
 type Universe.t = Level.t list (* hashconsed *)
+~~~
 
 The universe module defines modules and abstract types for levels,
 universes etc.. Structures are hashconsed (with a hack to take care
-of the fact that deserialization breaks sharing). 
+of the fact that deserialization breaks sharing).
 
-  Definitions (constants, inductives) now carry around not only 
+  Definitions (constants, inductives) now carry around not only
 constraints but also the universes they introduced (a Univ.UContext.t).
-There is another kind of contexts [Univ.ContextSet.t], the latter has 
+There is another kind of contexts `Univ.ContextSet.t`, the latter has
 a set of universes, while the former has serialized the levels in an
-array, and is used for polymorphic objects. Both have "reified" 
-constraints depending on global and local universes. 
+array, and is used for polymorphic objects. Both have "reified"
+constraints depending on global and local universes.
 
   A polymorphic definition is abstract w.r.t. the variables in this
 context, while a monomorphic one (or template polymorphic) just adds the
@@ -46,18 +47,18 @@ universes and constraints to the global universe context when it is put
 in the environment. No other universes than the global ones and the
 declared local ones are needed to check a declaration, hence the kernel
 does not produce any constraints anymore, apart from module
-subtyping.... There are hence two conversion functions now: [check_conv]
-and [infer_conv]: the former just checks the definition in the current env
+subtyping.... There are hence two conversion functions now: `check_conv`
+and `infer_conv`: the former just checks the definition in the current env
 (in which we usually push_universe_context of the associated context),
-and [infer_conv] which produces constraints that were not implied by the
+and `infer_conv` which produces constraints that were not implied by the
 ambient constraints. Ideally, that one could be put out of the kernel,
-but currently module subtyping needs it. 
+but currently module subtyping needs it.
 
  Inference of universes is now done during refinement, and the evar_map
 carries the incrementally built universe context, starting from the
-global universe constraints (see [Evd.from_env]). [Evd.conversion] is a
-wrapper around [infer_conv] that will do the bookkeeping for you, it
-uses [evar_conv_x]. There is a universe substitution being built
+global universe constraints (see `Evd.from_env`). `Evd.conversion` is a
+wrapper around `infer_conv` that will do the bookkeeping for you, it
+uses `evar_conv_x`. There is a universe substitution being built
 incrementally according to the constraints, so one should normalize at
 the end of a proof (or during a proof) with that substitution just like
 we normalize evars. There are some nf_* functions in
@@ -67,16 +68,16 @@ the universe constraints used in the term. It is heuristic but
 validity-preserving. No user-introduced universe (i.e. coming from a
 user-written anonymous Type) gets touched by this, only the fresh
 universes generated for each global application. Using
-
+~~~ocaml
 val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
-
+~~~
 Is the way to make a constr out of a global reference in the new API.
 If they constr is polymorphic, it will add the necessary constraints to
 the evar_map. Even if a constr is not polymorphic, we have to take care
 of keeping track of its universes. Typically, using:
-
-  mkApp (coq_id_function, [| A; a |]) 
-
+~~~ocaml
+  mkApp (coq_id_function, [| A; a |])
+~~~
 and putting it in a proof term is not enough now. One has to somehow
 show that A's type is in cumululativity relation with id's type
 argument, incurring a universe constraint. To do this, one can simply
@@ -84,19 +85,19 @@ call Typing.resolve_evars env evdref c which will do some infer_conv to
 produce the right constraints and put them in the evar_map. Of course in
 some cases you might know from an invariant that no new constraint would
 be produced and get rid of it. Anyway the kernel will tell you if you
-forgot some. As a temporary way out, [Universes.constr_of_global] allows
+forgot some. As a temporary way out, `Universes.constr_of_global` allows
 you to make a constr from any non-polymorphic constant, but it will fail
 on polymorphic ones.
 
 Other than that, unification (w_unify and evarconv) now take account of universes and
 produce only well-typed evar_maps.
 
-Some syntactic comparisons like the one used in [change] have to be
-adapted to allow identification up-to-universes (when dealing with 
-polymorphic references), [make_eq_univs_test] is there to help. 
+Some syntactic comparisons like the one used in `change` have to be
+adapted to allow identification up-to-universes (when dealing with
+polymorphic references), `make_eq_univs_test` is there to help.
 In constr, there are actually many new comparison functions to deal with
 that:
- 
+~~~ocaml
 (** [equal a b] is true if [a] equals [b] modulo alpha, casts,
    and application grouping *)
 val equal : constr -> constr -> bool
@@ -105,7 +106,7 @@ val equal : constr -> constr -> bool
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs : constr Univ.check_function
 
-(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
+(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
     alpha, casts, application grouping and the universe inequalities in [u]. *)
 val leq_constr_univs : constr Univ.check_function
 
@@ -120,47 +121,47 @@ val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained
 (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping and ignoring universe instances. *)
 val eq_constr_nounivs : constr -> constr -> bool
-
-The [_univs] versions are doing checking of universe constraints
-according to a graph, while the [_universes] are producing (non-atomic) 
+~~~
+The `_univs` versions are doing checking of universe constraints
+according to a graph, while the `_universes` are producing (non-atomic)
 universe constraints. The non-atomic universe constraints include the
-[ULub] constructor: when comparing [f (* u1 u2 *) c] and [f (* u1' u2'
-*) c] we add ULub constraints on [u1, u1'] and [u2, u2']. These are
-treated specially: as unfolding [f] might not result in these
+`ULub` constructor: when comparing `f (* u1 u2 *) c` and `f (* u1' u2'
+*) c` we add ULub constraints on `u1, u1'` and `u2, u2'`. These are
+treated specially: as unfolding `f` might not result in these
 unifications, we need to keep track of the fact that failure to satisfy
 them does not mean that the term are actually equal. This is used in
-unification but probably not necessary to the average programmer. 
+unification but probably not necessary to the average programmer.
 
 Another issue for ML programmers is that tables of constrs now usually
-need to take a [constr Univ.in_universe_context_set] instead, and
-properly refresh the universes context when using the constr, e.g. using 
-Clenv.refresh_undefined_univs clenv or: 
-
+need to take a `constr Univ.in_universe_context_set` instead, and
+properly refresh the universes context when using the constr, e.g. using
+Clenv.refresh_undefined_univs clenv or:
+~~~ocaml
 (** Get fresh variables for the universe context.
     Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : universe_context_set -> 
+val fresh_universe_context_set_instance : universe_context_set ->
   universe_level_subst * universe_context_set
-
-The substitution should be applied to the constr(s) under consideration, 
+~~~
+The substitution should be applied to the constr(s) under consideration,
 and the context_set merged with the current evar_map with:
-
+~~~ocaml
 val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
-
-The [rigid] flag here should be [Evd.univ_flexible] most of the
+~~~
+The `rigid` flag here should be `Evd.univ_flexible` most of the
 time. This means the universe levels of polymorphic objects in the
-constr might get instantiated instead of generating equality constraints 
+constr might get instantiated instead of generating equality constraints
 (Evd.univ_rigid does that).
 
-On this issue, I recommend forcing commands to take [global_reference]s
+On this issue, I recommend forcing commands to take `global_reference`s
 only, the user can declare his specialized terms used as hints as
 constants and this is cleaner. Alas, backward-compatibility-wise,
 this is the only solution I found. In the case of global_references
-only, it's just a matter of using [Evd.fresh_global] /
-[pf_constr_of_global] to let the system take care of universes.
+only, it's just a matter of using `Evd.fresh_global` /
+`pf_constr_of_global` to let the system take care of universes.
 
 
 The universe graph
-==================
+------------------
 
 To accomodate universe polymorphic definitions, the graph structure in
 kernel/univ.ml was modified. The new API forces every universe to be
@@ -176,68 +177,14 @@ no universe i can be set lower than Set, so the chain of universes
 always bottoms down at Prop < Set.
 
 Modules
-=======
+-------
 
 One has to think of universes in modules as being globally declared, so
 when including a module (type) which declares a type i (e.g. through a
 parameter), we get back a copy of i and not some fresh universe.
 
-Projections
-===========
-
-  | Proj of constant * constr
-
-Projections are always applied to a term, which must be of a record type
-(i.e. reducible to an inductive type [I params]). Type-checking,
-reduction and conversion are fast (not as fast as they could be yet)
-because we don't keep parameters around. As you can see, it's currently
-a [constant] that is used here to refer to the projection, that will
-change to an abstract [projection] type in the future. Basically a
-projection constant records which inductive it is a projection for, the
-number of params and the actual position in the constructor that must be
-projected. For compatibility reason, we also define an eta-expanded form
-(accessible from user syntax @f). The constant_entry of a projection has
-both informations. Declaring a record (under [Set Primitive
-Projections]) will generate such definitions. The API to declare them is
-not stable at the moment, but the inductive type declaration also knows
-about the projections, i.e. a record inductive type decl contains an
-array of terms representing the projections. This is used to implement
-eta-conversion for record types (with at least one field and having all
-projections definable). The canonical value being [Build_R (pn x)
-... (pn x)]. Unification and conversion work up to this eta rule. The
-records can also be universe polymorphic of course, and we don't need to
-keep track of the universe instance for the projections either.
-Projections are reduced _eagerly_ everywhere, and introduce a new Zproj
-constructor in the abstract machines that obeys both the delta (for the
-constant opacity) and iota laws (for the actual reduction). Refolding
-works as well (afaict), but there is a slight hack there related to
-universes (not projections). 
-
-For the ML programmer, the biggest change is that pattern-matchings on
-kind_of_term require an additional case, that is handled usually exactly
-like an [App (Const p) arg].
-
-There are slight hacks related to hints is well, to use the primitive
-projection form of f when one does [Hint Resolve f]. Usually hint
-resolve will typecheck the term, resulting in a partially applied
-projection (disallowed), so we allow it to take
-[constr_or_global_reference] arguments instead and special-case on
-projections. Other tactic extensions might need similar treatment. 
-
-WIP
-===
-
-- [vm_compute] does not deal with universes and projections correctly,
-except when it goes to a normal form with no projections or polymorphic
-constants left (the most common case). E.g. Ring with Set Universe
-Polymorphism and Set Primitive Projections work (at least it did at some
-point, I didn't recheck yet).  
-
-- [native_compute] works with universes and projections.
-
-
 Incompatibilities
-=================
+-----------------
 
 Old-style universe polymorphic definitions were implemented by taking
 advantage of the fact that elaboration (i.e., pretyping and unification)
@@ -247,33 +194,33 @@ possible, as unification ensures that the substitution is built is
 entirely well-typed, even w.r.t universes. This means that some terms
 that type-checked before no longer do, especially projections of the
 pair:
-
+~~~coq
 @fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)).
-
+~~~
 The "template universe polymorphic" variables i and j appear during
 typing without being refreshed, meaning that they can be lowered (have
 upper constraints) with user-introduced universes. In most cases this
 won't work, so ?x and ?y have to be instantiated earlier, either from
 the type of the actual projected pair term (some t : prod A B) or the
-typing constraint. Adding the correct type annotations will always fix 
+typing constraint. Adding the correct type annotations will always fix
 this.
 
 
 Unification semantics
-=====================
+---------------------
 
 In Ltac, matching with:
 
-- a universe polymorphic constant [c] matches any instance of the
+- a universe polymorphic constant `c` matches any instance of the
   constant.
-- a variable ?x already bound to a term [t] (non-linear pattern) uses 
+- a variable ?x already bound to a term `t` (non-linear pattern) uses
   strict equality of universes (e.g., Type@{i} and Type@{j} are not
   equal).
 
 In tactics:
 
-- [change foo with bar], [pattern foo] will unify all instances of [foo]
-  (and convert them with [bar]). This might incur unifications of
-  universes. [change] uses conversion while [pattern] only does
+- `change foo with bar`, `pattern foo` will unify all instances of `foo`
+  (and convert them with `bar`). This might incur unifications of
+  universes. `change` uses conversion while `pattern` only does
   syntactic matching up-to unification of universes.
-- [apply], [refine] use unification up to universes.
+- `apply`, `refine` use unification up to universes.
diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt
deleted file mode 100644
index a40706e9..00000000
--- a/dev/doc/universes.txt
+++ /dev/null
@@ -1,26 +0,0 @@
-How to debug universes?
-
-1. There is a command Print Universes in Coq toplevel
-
-   Print Universes.
-     prints the graph of universes in the form of constraints
-
-   Print Universes "file".
-     produces the "file" containing universe constraints in the form
-       univ1 # univ2 ;
-     where # can be either > >= or =
-
-   If "file" ends with .gv or .dot, the resulting file will be in
-   dot format.
-
-
-   *) for dot see http://www.research.att.com/sw/tools/graphviz/
-
-
-2. There is a printing option
-
-   {Set,Unset} Printing Universes.
-
-   which, when set, makes all pretty-printed Type's annotated with the
-   name of the universe.
-
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 492e75a7..3867d4af 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -376,9 +376,27 @@ Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation
 && \feature{new proof engine deployed} [2-11-2013]\\
 && \feature{universe polymorphism} [6-5-2014]\\
 && \feature{primitive projections} [6-5-2014]\\
+&& \feature{miscellaneous optimizations}\\
 
 Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\
 
+Coq V8.5 & released 22 January 2016 & \\
+
+Coq V8.6 beta 1 & released 19 November 2016 & \feature{irrefutable patterns} [15-2-2016]\\
+&& \feature{Ltac profiling} [14-6-2016]\\
+&& \feature{warning system} [29-6-2016]\\
+&& \feature{miscellaneous optimizations}\\
+
+Coq V8.6 & released 14 December 2016 & \\
+
+Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect plugin} [6-6-2017]\\
+&& \feature{cumulative polymorphic inductive types} [19-6-2017]\\
+&& \feature{further optimizations}\\
+
+Coq V8.7 beta 2 & released 6 October 2017 & \\
+
+Coq V8.7 & released 18 October 2016 & \\
+
 \end{tabular}
 
 \medskip
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
new file mode 100644
index 00000000..b35571e9
--- /dev/null
+++ b/dev/doc/xml-protocol.md
@@ -0,0 +1,755 @@
+# Coq XML Protocol
+
+This document is based on documentation originally written by CJ Bell
+for his [vscoq](https://github.com/siegebell/vscoq/) project.
+
+Here, the aim is to provide a "hands on" description of the XML
+protocol that coqtop and IDEs use to communicate. The protocol first appeared 
+with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming 
+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).
+
+Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt).
+
+* [Commands](#commands)
+  - [About](#command-about)
+  - [Add](#command-add)
+  - [EditAt](#command-editAt)
+  - [Init](#command-init)
+  - [Goal](#command-goal)
+  - [Status](#command-status)
+  - [Query](#command-query)
+  - [Evars](#command-evars)
+  - [Hints](#command-hints)
+  - [Search](#command-search)
+  - [GetOptions](#command-getoptions)
+  - [SetOptions](#command-setoptions)
+  - [MkCases](#command-mkcases)
+  - [StopWorker](#command-stopworker)
+  - [PrintAst](#command-printast)
+  - [Annotate](#command-annotate)
+* [Feedback messages](#feedback)
+  - [Added Axiom](#feedback-addedaxiom)
+  - [Processing](#feedback-processing)
+  - [Processed](#feedback-processed)
+  - [Incomplete](#feedback-incomplete)
+  - [Complete](#feedback-complete)
+  - [GlobRef](#feedback-globref)
+  - [Error](#feedback-error)
+  - [InProgress](#feedback-inprogress)
+  - [WorkerStatus](#feedback-workerstatus)
+  - [File Dependencies](#feedback-filedependencies)
+  - [File Loaded](#feedback-fileloaded)
+  - [Message](#feedback-message)
+  - [Custom](#feedback-custom)
+
+Sentences: each command sent to Coqtop is a "sentence"; they are typically terminated by ".\s" (followed by whitespace or EOF).
+Examples: "Lemma a: True.", "(* asdf *) Qed.", "auto; reflexivity."
+In practice, the command sentences sent to Coqtop are terminated at the "." and start with any previous whitespace.
+Each sentence is assigned a unique stateId after being sent to Coq (via Add).
+States:
+  * Processing: has been received by Coq and has no obvious syntax error (that would prevent future parsing)
+  * Processed:
+  * InProgress:
+  * Incomplete: the validity of the sentence cannot be checked due to a prior error
+  * Complete:
+  * Error: the sentence has an error
+
+State ID 0 is reserved as a 'dummy' state.
+
+--------------------------
+
+## <a name="commands">Commands</a>
+
+### <a name="command-about">**About(unit)**</a>
+Returns information about the protocol and build dates for Coqtop.
+```
+<call val="About">
+  <unit/>
+</call>
+```
+#### *Returns*
+```html
+ <value val="good">
+   <coq_info><string>8.6</string>
+     <string>20150913</string>
+     <string>December 2016</string>
+     <string>Dec 23 2016 16:16:30</string>
+   </coq_info>
+</value>
+```
+The string fields are the Coq version, the protocol version, the release date, and the compile time of Coqtop.
+The protocol version is a date in YYYYMMDD format, where "20150913" corresponds to Coq 8.6. An IDE that wishes 
+to support multiple Coq versions can use the protocol version information to know how to handle output from Coqtop.
+
+### <a name="command-add">**Add(stateId: integer, command: string, verbose: boolean)**</a>
+Adds a toplevel command (e.g. vernacular, definition, tactic) to the given state.
+`verbose` controls whether out-of-band messages will be generated for the added command (e.g. "foo is assumed" in response to adding "Axiom foo: nat.").
+```html
+<call val="Add">
+  <pair>
+    <pair>
+      <string>${command}</string>
+      <int>${editId}</int>
+    </pair>
+    <pair>
+      <state_id val="${stateId}"/>
+      <bool val="${verbose}"/>
+    </pair>
+  </pair>
+</call>
+```
+
+#### *Returns*
+* The added command is given a fresh `stateId` and becomes the next "tip".
+```html
+<value val="good">
+  <pair>
+    <state_id val="${newStateId}"/>
+    <pair>
+      <union val="in_l"><unit/></union>
+      <string>${message}</string>
+    </pair>
+  </pair>
+</value>
+```
+* When closing a focused proof (in the middle of a bunch of interpreted commands),
+the `Qed` will be assigned a prior `stateId` and `nextStateId` will be the id of an already-interpreted
+state that should become the next tip. 
+```html
+<value val="good">
+  <pair>
+    <state_id val="${stateId}"/>
+    <pair>
+      <union val="in_r"><state_id val="${nextStateId}"/></union>
+      <string>${message}</string>
+    </pair>
+  </pair>
+</value>
+```
+* Failure:
+  - Syntax error. Error offsets are byte offsets (not character offsets) with respect to the start of the sentence, starting at 0.
+  ```html
+  <value val="fail"
+      loc_s="${startOffsetOfError}"
+      loc_e="${endOffsetOfError}">
+    <state_id val="${stateId}"/>
+    <richpp>${errorMessage}</richpp>
+  </value>
+  ```
+  - Another kind of error, for example, Qed with a pending goal.	
+  ```html
+  <value val="fail"><state_id val="${stateId}"/><richpp>${errorMessage}</richpp></value>
+  ```
+
+-------------------------------
+
+### <a name="command-editAt">**EditAt(stateId: integer)**</a>
+Moves current tip to `${stateId}`, such that commands may be added to the new state ID.
+```html
+<call val="Edit_at"><state_id val="${stateId}"/></call>
+```
+#### *Returns*
+* Simple backtrack; focused stateId becomes the parent state
+```html
+<value val="good">
+  <union val="in_l"><unit/></union>
+</value>
+```
+
+* New focus; focusedQedStateId is the closing Qed of the new focus; senteneces between the two should be cleared
+```html
+<value val="good">
+  <union val="in_r">
+    <pair>
+      <state_id val="${focusedStateId}"/>
+      <pair>
+        <state_id val="${focusedQedStateId}"/>
+        <state_id val="${oldFocusedStateId}"/>
+      </pair>
+    </pair>
+  </union>
+</value>
+```
+* Failure: If `stateId` is in an error-state and cannot be jumped to, `errorFreeStateId` is the parent state of ``stateId` that shopuld be edited instead. 
+```html
+<value val="fail" loc_s="${startOffsetOfError}" loc_e="${endOffsetOfError}">
+  <state_id val="${errorFreeStateId}"/>
+  ${errorMessage}
+</value>
+```
+
+-------------------------------
+
+### <a name="command-init">**Init()**</a>
+* No options.
+```html
+<call val="Init"><option val="none"/></call>
+```
+* With options. Looking at
+  [ide_slave.ml](https://github.com/coq/coq/blob/c5d0aa889fa80404f6c291000938e443d6200e5b/ide/ide_slave.ml#L355),
+  it seems that `options` is just the name of a script file, whose path
+  is added via `Add LoadPath` to the initial state.
+```html
+<call val="Init">
+  <option val="some">
+    <string>${options}</string>
+  </option>
+</call>
+```
+Providing the script file enables Coq to use .aux files created during
+compilation. Those file contain timing information that allow Coq to
+choose smartly between asynchronous and synchronous processing of
+proofs.
+
+#### *Returns*
+* The initial stateId (not associated with a sentence)
+```html
+<value val="good">
+  <state_id val="${initialStateId}"/>
+</value>
+```
+
+-------------------------------
+
+
+### <a name="command-goal">**Goal()**</a>
+```html
+<call val="Goal"><unit/></call>
+```
+#### *Returns*
+* If there is a goal. `shelvedGoals` and `abandonedGoals` have the same structure as the first set of (current/foreground) goals. `backgroundGoals` contains a list of pairs of lists of goals (list ((list Goal)*(list Goal))); it represents a "focus stack" ([see code for reference](https://github.com/coq/coq/blob/trunk/engine/proofview.ml#L113)). Each time a proof is focused, it will add a new pair of lists-of-goals. The first pair is the most nested set of background goals, the last pair is the top level set of background goals. The first list in the pair is in reverse order. Each time you focus the goal (e.g. using `Focus` or a bullet), a new pair will be prefixed to the list.
+```html
+<value val="good">
+  <option val="some">
+  <goals>
+    <!-- current goals -->
+    <list>
+      <goal>
+        <string>3</string>
+        <list>
+          <richpp>${hyp1}</richpp>
+          ...
+          <richpp>${hypN}</richpp>
+        </list>
+        <richpp>${goal}</richpp>
+      </goal>
+      ...
+      ${goalN}
+    </list>
+    <!-- `backgroundGoals` -->
+    <list>
+      <pair>
+        <list><goal />...</list>
+        <list><goal />...</list>
+      </pair>
+      ...
+    </list>
+    ${shelvedGoals}
+    ${abandonedGoals}
+  </goals>
+  </option>
+</value>
+```
+
+For example, this script:
+```coq
+Goal P -> (1=1/\2=2) /\ (3=3 /\ (4=4 /\ 5=5) /\ 6=6) /\ 7=7.
+intros.
+split; split. (* current visible goals are [1=1, 2=2, 3=3/\(4=4/\5=5)/\6=6, 7=7] *)
+Focus 3. (* focus on 3=3/\(4=4/\5=5)/\6=6; bg-before: [1=1, 2=2], bg-after: [7=7] *)
+split; [ | split ]. (* current visible goals are [3=3, 4=4/\5=5, 6=6] *)
+Focus 2. (* focus on 4=4/\5=5; bg-before: [3=3], bg-after: [6=6] *)
+* (* focus again on 4=4/\5=5; bg-before: [], bg-after: [] *)
+split. (* current visible goals are [4=4,5=5] *)
+```
+should generate the following goals structure:
+```
+goals: [ P|-4=4, P|-5=5 ]
+background:
+[
+  ( [], [] ), (* bullet with one goal has no before or after background goals *)
+  ( [ P|-3=3 ], [ P|-6=6 ] ), (* Focus 2 *)
+  ( [ P|-2=2, P|-1=1 ], [ P|-7=7 ] ) (* Focus 3; notice that 1=1 and 2=2 are reversed *)
+]
+```
+Pseudocode for listing all of the goals in order: `rev (flat_map fst background) ++ goals ++ flat_map snd background`.
+
+* No goal:
+```html
+<value val="good"><option val="none"/></value>
+```
+
+-------------------------------
+
+
+### <a name="command-status">**Status(force: bool)**</a>
+Returns information about the current proofs. CoqIDE typically sends this
+message with `force = false` after each sentence, and with `force = true` if
+the user wants to force the checking of all proofs (wheels button). In terms of
+the STM API, `force` triggers a `Join`.
+```html
+<call val="Status"><bool val="${force}"/></call>
+```
+#### *Returns*
+*  
+```html
+<status>
+  <string>${path}</string>
+  <string>${proofName}</string>
+  <string>${allProofs}</string>
+  <string>${proofNumber}</string>
+</status>
+```
+
+-------------------------------
+
+### <a name="command-query">**Query(route_id: integer, query: string, stateId: integer)**</a>
+
+`routeId` can be used to distinguish the result of a particular query,
+`stateId` should be set to the state the query should be run.
+
+```html
+<call val="Query">
+  <pair>
+    <route_id val="${routeId}"/>
+  <pair>
+    <string>${query}</string>
+    <state_id val="${stateId}"/>
+  </pair>
+  </pair>
+</call>
+```
+#### *Returns*
+*
+```html
+<value val="good">
+  <string>${message}</string>
+</value>
+```
+
+Before 8.8, `Query` only executed the first command present in the
+`query` string; starting with 8.8, the caller may include several
+statements. This is useful for instance for temporarily setting an
+option and then executing a command.
+
+-------------------------------
+
+
+
+### <a name="command-evars">**Evars()**</a>
+```html
+<call val="Evars"><unit/></call>
+```
+#### *Returns*
+*
+```html
+<value val="good">
+  <option val="some">
+    <list>
+      <evar>${evar1}</evar>
+      ...
+      <evar>${evarN}</evar>
+    </list>
+  </option>
+</value>
+```
+
+-------------------------------
+
+
+### <a name="command-hints">**Hints()**</a>
+```html
+<call val="Hints"><unit/></call>
+```
+#### *Returns*
+*
+```html
+<value val="good">
+  <option val="some">
+    <pair>
+      <list/>
+      <list>
+        <pair>
+          <string>${hint1}</string>
+          <string>${hint2}</string>
+        </pair>
+        ...
+        <pair>
+          <string>${hintN-1}</string>
+          <string>${hintN}</string>
+        </pair>
+      </list>
+    </pair>
+  </option>
+</value>
+```
+
+-------------------------------
+
+
+### <a name="command-search">**Search([(constraintTypeN: string, constraintValueN: string, positiveConstraintN: boolean)])**</a>
+Searches for objects that satisfy a list of constraints. If `${positiveConstraint}` is `false`, then the constraint is inverted. 
+```html
+<call val="Search">
+  <list>
+    <pair>
+      <search_cst val="${constraintType1}">
+        ${constraintValue1}
+      </search_cst>
+      <bool val="${positiveConstraint1}"/>
+    </pair>
+    ...
+    <!-- Example: -->
+    <pair>
+      <search_cst val="name_pattern">
+        <string>bool_rect</string>
+      </search_cst>
+      <bool val="true"/>
+    </pair>
+  </list>
+</call>
+```
+#### *Returns*
+*
+```html
+<value val="good">
+  <list>
+      <coq_object>
+          <list>
+              <string>${metaInfo}</string>
+              ...
+          </list>
+          <list>
+              <string>${name}</string>
+          </list>
+          <string>${definition}</string>
+      </coq_object>
+      ...
+  </list>
+</value>
+```
+##### Types of constraints:
+* Name pattern: `${constraintType} = "name_pattern"`; `${constraintValue}` is a regular expression string.
+* Type pattern: `${constraintType} = "type_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string.
+* SubType pattern: `${constraintType} = "subtype_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string.
+* In module: `${constraintType} = "in_module"`; `${constraintValue}` is a list of strings specifying the module/directory structure.
+* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is ommitted*.
+
+-------------------------------
+
+
+### <a name="command-getoptions">**GetOptions()**</a>
+```html
+<call val="GetOptions"><unit/></call>
+```
+#### *Returns*
+*
+```html
+<value val="good">
+  <list>
+    <pair>
+      <list><string>${string1}</string>...</list>
+      <option_state>
+        <bool>${sync}</bool>
+        <bool>${deprecated}</bool>
+        <string>${name}</string>
+        ${option_value}
+      </option_state>
+    </pair>
+    ...
+  </list>
+</value>
+```
+
+-------------------------------
+
+
+### <a name="command-setoptions">**SetOptions(options)**</a>
+Sends a list of option settings, where each setting roughly looks like:
+`([optionNamePart1, ..., optionNamePartN], value)`.
+```html
+<call val="SetOptions">
+  <list>
+    <pair>
+      <list>
+        <string>optionNamePart1</string>
+        ...
+        <string>optionNamePartN</string>
+      </list>
+      <option_value val="${typeOfOption}">
+        <option val="some">
+          ${value}
+        </option>
+      </option_value>
+    </pair>
+    ...
+    <!-- Example: -->
+    <pair>
+      <list>
+        <string>Printing</string>
+        <string>Width</string>
+      </list>
+      <option_value val="intvalue">
+        <option val="some"><int>60</int></option>
+      </option_value>
+    </pair>
+  </list>
+</call>
+```
+CoqIDE sends the following settings (defaults in parentheses):
+```
+Printing Width : (<option_value val="intvalue"><int>60</int></option_value>),
+Printing Coercions : (<option_value val="boolvalue"><bool val="false"/></option_value>),
+Printing Matching : (...true...)
+Printing Notations : (...true...)
+Printing Existential Instances : (...false...)
+Printing Implicit : (...false...)
+Printing All : (...false...)
+Printing Universes : (...false...)
+```
+#### *Returns*
+*
+```html
+<value val="good"><unit/></value>
+```
+
+-------------------------------
+
+
+### <a name="command-mkcases">**MkCases(...)**</a>
+```html
+<call val="MkCases"><string>...</string></call>
+```
+#### *Returns*
+*
+```html
+<value val="good">
+  <list>
+    <list><string>${string1}</string>...</list>
+    ...
+  </list>
+</value>
+```
+
+-------------------------------
+
+
+### <a name="command-stopworker">**StopWorker(worker: string)**</a>
+```html
+<call val="StopWorker"><string>${worker}</string></call>
+```
+#### *Returns*
+*
+```html
+<value val="good"><unit/></value>
+```
+
+-------------------------------
+
+
+### <a name="command-printast">**PrintAst(stateId: integer)**</a>
+```html
+<call val="PrintAst"><state_id val="${stateId}"/></call>
+```
+#### *Returns*
+*
+```html
+<value val="good">
+  <gallina begin="${gallina_begin}" end="${gallina_end}">
+    <theorem begin="${theorem_begin}" end="${theorem_end}" type="Theorem" name="${theorem_name}">
+      <apply begin="${apply_begin}" end="${apply_end}">
+        <operator begin="${operator_begin}" end="${operator_end}" name="${operator_name}"/>
+        <typed begin="${typed_begin}" end="${typed_end}">
+          <constant begin="${constant_begin}" end="${constant_end}" name="${constant_name}"/>
+          ...
+          <token begin="${token_begin}" end="token_end">${token}</token>
+          ...
+        </typed>
+        ...
+      </apply>
+    </theorem>
+    ...
+  </gallina>
+</value>
+```
+
+-------------------------------
+
+
+
+### <a name="command-annotate">**Annotate(annotation: string)**</a>
+```html
+<call val="Annotate"><string>${annotation}</string></call>
+```
+#### *Returns*
+*
+
+take `<call val="Annotate"><string>Theorem plus_0_r : forall n : nat, n + 0 = n.</string></call>` as an example.
+
+```html
+<value val="good">
+  <pp startpos="0" endpos="45">
+    <vernac_expr startpos="0" endpos="44">
+      <keyword startpos="0" endpos="7">Theorem</keyword>
+      &nbsp;plus_0_r&nbsp;:&nbsp;
+      <constr_expr startpos="19" endpos="44">
+        <keyword startpos="19" endpos="25">forall</keyword>
+        &nbsp;n&nbsp;:&nbsp;
+        <constr_expr startpos="30" endpos="33">nat</constr_expr>
+        ,&nbsp;
+        <unparsing startpos="35" endpos="44">
+          <unparsing startpos="35" endpos="40">
+            <unparsing startpos="35" endpos="40">
+              <unparsing startpos="35" endpos="36">
+                <constr_expr startpos="35" endpos="36">n</constr_expr>
+              </unparsing>
+              <unparsing startpos="36" endpos="38">&nbsp;+</unparsing>
+              <unparsing startpos="38" endpos="39">&nbsp;</unparsing>
+              <unparsing startpos="39" endpos="40">
+                <constr_expr startpos="39" endpos="40">0</constr_expr>
+              </unparsing>
+            </unparsing>
+          </unparsing>
+          <unparsing startpos="40" endpos="42">&nbsp;=</unparsing>
+          <unparsing startpos="42" endpos="43">&nbsp;</unparsing>
+          <unparsing startpos="43" endpos="44">
+            <constr_expr startpos="43" endpos="44">n</constr_expr>
+          </unparsing>
+        </unparsing>
+      </constr_expr>
+    </vernac_expr>
+    .
+  </pp>
+</value>
+```
+
+-------------------------------
+
+## <a name="feedback">Feedback messages</a>
+
+Feedback messages are issued out-of-band,
+  giving updates on the current state of sentences/stateIds,
+  worker-thread status, etc.
+
+In the descriptions of feedback syntax below, wherever a `state_id`
+tag may occur, there may instead be an `edit_id` tag.
+
+* <a name="feedback-addedaxiom">Added Axiom</a>: in response to `Axiom`, `admit`, `Admitted`, etc.
+```html
+<feedback object="state" route="0">
+  <state_id val="${stateId}"/>
+  <feedback_content val="addedaxiom" />
+</feedback>
+```
+* <a name="feedback-processing">Processing</a>
+```html
+<feedback object="state" route="0">
+  <state_id val="${stateId}"/>
+  <feedback_content val="processingin">
+    <string>${workerName}</string>
+  </feedback_content>
+</feedback>
+```
+* <a name="feedback-processed">Processed</a>
+```html
+<feedback object="state" route="0">
+  <feedback object="state" route="0">
+    <state_id val="${stateId}"/>
+  <feedback_content val="processed"/>
+</feedback>
+```
+* <a name="feedback-incomplete">Incomplete</a>
+```html
+<feedback object="state" route="0">
+  <state_id val="${stateId}"/>
+  <feedback_content val="incomplete" />
+</feedback>
+```
+* <a name="feedback-complete">Complete</a>
+* <a name="feedback-globref">GlobRef</a>
+* <a name="feedback-error">Error</a>. Issued, for example, when a processed tactic has failed or is unknown.
+The error offsets may both be 0 if there is no particular syntax involved.
+* <a name="feedback-inprogress">InProgress</a>
+```html
+<feedback object="state" route="0">
+  <state_id val="${stateId}"/>
+  <feedback_content val="inprogress">
+    <int>1</int>
+  </feedback_content>
+</feedback>
+```
+* <a name="feedback-workerstatus">WorkerStatus</a>
+Ex: `workername = "proofworker:0"`
+Ex: `status = "Idle"` or `status = "proof: myLemmaName"` or `status = "Dead"`
+```html
+<feedback object="state" route="0">
+  <state_id val="${stateId}"/>
+  <feedback_content val="workerstatus">
+    <pair>
+      <string>${workerName}</string>
+      <string>${status}</string>
+    </pair>
+  </feedback_content>
+</feedback>
+```
+* <a name="feedback-filedependencies">File Dependencies</a>. Typically in response to a `Require`. Dependencies are *.vo files.
+  - State `stateId` directly depends on `dependency`:
+  ```html
+  <feedback object="state" route="0">
+    <state_id val="${stateId}"/>
+    <feedback_content val="filedependency">
+      <option val="none"/>
+      <string>${dependency}</string>
+    </feedback_content>
+  </feedback>
+  ```
+  - State `stateId` depends on `dependency` via dependency `sourceDependency`
+  ```xml
+  <feedback object="state" route="0">
+    <state_id val="${stateId}"/>
+    <feedback_content val="filedependency">
+      <option val="some"><string>${sourceDependency}</string></option>
+      <string>${dependency}</string>
+    </feedback_content>
+  </feedback>
+  ```
+* <a name="feedback-fileloaded">File Loaded</a>. For state `stateId`, module `module` is being loaded from `voFileName`
+```xml
+<feedback object="state" route="0">
+  <state_id val="${stateId}"/>
+  <feedback_content val="fileloaded">
+    <string>${module}</string>
+    <string>${voFileName`}</string>
+  </feedback_content>
+</feedback>
+```
+
+* <a name="feedback-message">Message</a>. `level` is one of `{info,warning,notice,error,debug}`. For example, in response to an <a href="#command-add">add</a> `"Axiom foo: nat."` with `verbose=true`, message `foo is assumed` will be emitted in response.
+```xml
+<feedback object="state" route="0">
+  <state_id val="${stateId}"/>
+  <feedback_content val="message">
+    <message>
+      <message_level val="${level}"/>
+      <string>${message}</string>
+    </message>
+  </feedback_content>
+</feedback>
+```
+
+* <a name="feedback-custom">Custom</a>. A feedback message that Coq plugins can use to return structured results, including results from Ltac profiling. Optionally, `startPos` and `stopPos` define a range of offsets in the document that the message refers to; otherwise, they will be 0. `customTag` is intended as a unique string that identifies what kind of payload is contained in `customXML`.
+```xml
+<feedback object="state" route="0">
+  <state_id val="${stateId}"/>
+  <feedback_content val="custom">
+    <loc start="${startPos}" stop="${stopPos}"/>
+    <string>${customTag}</string>
+    ${customXML}
+  </feedback_content>
+</feedback>
+```
+