16 files changed, 151 insertions, 213 deletions
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index c450e8157a..3a096fec06 100755
--- a/dev/build/osx/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
@@ -4,7 +4,6 @@
 set -e
 
 # Configuration setup
-OUTDIR=$PWD/_install
 DMGDIR=$PWD/_dmg
 VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
 APP=bin/CoqIDE_${VERSION}.app
@@ -13,7 +12,7 @@ APP=bin/CoqIDE_${VERSION}.app
 make PRIVATEBINARIES="$APP" -j "$NJOBS" -l2 "$APP"
 
 # Add Coq to the .app file
-make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources/" install-coq install-ide-toploop
+make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources" install-coq install-ide-toploop
 
 # Create the dmg bundle
 mkdir -p "$DMGDIR"
diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md
index 01769aeddb..06b617d4c1 100644
--- a/dev/ci/README-users.md
+++ b/dev/ci/README-users.md
@@ -45,6 +45,26 @@ using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is
 to give merge permissions to someone from the Coq team as to help with
 these kind of merges.
 
+### OCaml and plugin-specific considerations
+
+Developments that link against Coq's OCaml API [most of them are known
+as "plugins"] do have some special requirements:
+
+- Coq's OCaml API is not stable. We hope to improve this in the future
+  but as of today you should expect to have to merge a fair amount of
+  "overlays", usually in the form of Pull Requests from Coq developers
+  in order to keep your plugin compatible with Coq master.
+
+  In order to alleviate the load, you can delegate the merging of such
+  compatibility pull requests to Coq developers themselves, by
+  granting access to the plugin repository or by using `bots` such as
+  [Bors](https://github.com/apps/bors) that allow for automatic
+  management of Pull Requests.
+
+- Plugins in the CI should compile with the OCaml flags that Coq
+  uses. In particular, warnings that are considered fatal by the Coq
+  developers _must_ be also fatal for plugin CI code.
+
 ### Add your development by submitting a pull request
 
 Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 0c89809ee9..4f5988c59c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -254,7 +254,7 @@
 : "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}"
 
 ########################################################################
-# relation-algebra
+# relation_algebra
 ########################################################################
 : "${relation_algebra_CI_REF:=master}"
 : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index b4d2a9ca4e..7aa265cf90 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -108,10 +108,9 @@ install_ssreflect()
 
   git_download mathcomp
 
-  ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
-    make Makefile.coq && \
-    make -f Makefile.coq ssreflect/all_ssreflect.vo && \
-    make -f Makefile.coq install )
+  ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp/ssreflect" && \
+    make && \
+    make install )
 
 }
 
@@ -123,8 +122,11 @@ install_ssralg()
   git_download mathcomp
 
   ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
-    make Makefile.coq && \
-    make -f Makefile.coq algebra/all_algebra.vo && \
-    make -f Makefile.coq install )
+    make -C ssreflect && \
+    make -C ssreflect install && \
+    make -C fingroup && \
+    make -C fingroup install && \
+    make -C algebra && \
+    make -C algebra install )
 
 }
diff --git a/dev/ci/ci-relation-algebra.sh b/dev/ci/ci-relation_algebra.sh
index 84bed5bdfe..84bed5bdfe 100755
--- a/dev/ci/ci-relation-algebra.sh
+++ b/dev/ci/ci-relation_algebra.sh
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e553cbed1b..8eebb3af64 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-03-12-V1"
+# CACHEKEY: "bionic_coq-V2019-04-20-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -38,7 +38,7 @@ ENV COMPILER="4.05.0"
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
-    CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8"
+    CI_OPAM="menhir.20181113 elpi.1.2.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
diff --git a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
new file mode 100644
index 0000000000..67f6f8610a
--- /dev/null
+++ b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "8764" ] || [ "$CI_BRANCH" = "master-parsing-decimal" ]; then
+
+    ltac2_CI_REF=master-parsing-decimal
+    ltac2_CI_GITURL=https://github.com/proux01/ltac2
+
+    quickchick_CI_REF=master-parsing-decimal
+    quickchick_CI_GITURL=https://github.com/proux01/QuickChick
+
+    Corn_CI_REF=master-parsing-decimal
+    Corn_CI_GITURL=https://github.com/proux01/corn
+
+    HoTT_CI_REF=master-parsing-decimal
+    HoTT_CI_GITURL=https://github.com/proux01/HoTT
+
+    stdlib2_CI_REF=master-parsing-decimal
+    stdlib2_CI_GITURL=https://github.com/proux01/stdlib2
+
+fi
diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
new file mode 100644
index 0000000000..12be1b676a
--- /dev/null
+++ b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then
+
+    HoTT_CI_REF=rm-hardwired-hint-db
+    HoTT_CI_GITURL=https://github.com/vbgl/HoTT
+
+    ltac2_CI_REF=rm-hardwired-hint-db
+    ltac2_CI_GITURL=https://github.com/vbgl/ltac2
+
+    UniMath_CI_REF=rm-hardwired-hint-db
+    UniMath_CI_GITURL=https://github.com/vbgl/UniMath
+
+fi
diff --git a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh
new file mode 100644
index 0000000000..1e1d36d54a
--- /dev/null
+++ b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9165" ] || [ "$CI_BRANCH" = "recarg-cleanup" ]; then
+
+    elpi_CI_REF=recarg-cleanup
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    quickchick_CI_REF=recarg-cleanup
+    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
new file mode 100644
index 0000000000..01d3068591
--- /dev/null
+++ b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
@@ -0,0 +1,21 @@
+if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then
+
+    elpi_CI_REF=pretyping-rm-global
+    elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+    coqhammer_CI_REF=pretyping-rm-global
+    coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer
+
+    equations_CI_REF=pretyping-rm-global
+    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+    ltac2_CI_REF=pretyping-rm-global
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    paramcoq_CI_REF=pretyping-rm-global
+    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
+
+    mtac2_CI_REF=pretyping-rm-global
+    mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh
new file mode 100644
index 0000000000..9a6e25d893
--- /dev/null
+++ b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9973" ] || [ "$CI_BRANCH" = "elpi-1.2" ]; then
+
+    elpi_CI_REF=overlay-elpi1.2-coq-master
+    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
+
+fi
diff --git a/dev/doc/archive/COMPATIBILITY b/dev/doc/archive/COMPATIBILITY
index a81afca32d..35a7f608de 100644
--- a/dev/doc/archive/COMPATIBILITY
+++ b/dev/doc/archive/COMPATIBILITY
@@ -1,192 +1,6 @@
 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...
 
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 416253fad1..4533a4dc01 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -20,6 +20,15 @@ General deprecation
   removed. Please, make sure your plugin is warning-free in 8.8 before
   trying to port it over 8.9.
 
+Warnings
+
+- Coq now builds plugins with `-warn-error` enabled by default. The
+  amount of dangerous warnings in plugin code was very high, so we now
+  require plugins in the CI to adhere to the Coq warning policy. We
+  _strongly_ recommend against disabling the default set of warnings.
+  If you have special needs, see the documentation of your build
+  system and/or OCaml for further help.
+
 Names
 
 - Kernel names no longer contain a section path. They now have only two
@@ -83,6 +92,11 @@ Libobject
   * `Libobject.superglobal_object`
   * `Libobject.superglobal_object_nodischarge`
 
+AST
+
+- Minor changes in the AST have been performed, for example
+  https://github.com/coq/coq/pull/9165
+
 Implicit Arguments
 
 - `Impargs.declare_manual_implicits` is restricted to only support declaration
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index c0a5b9095c..01c2b574a2 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -195,6 +195,18 @@ Conversion machines
   GH issue number: ?
   risk: 
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: primitive integer emulation layer on 32 bits not robust to garbage collection
+  introduced: master (before v8.10 in GH pull request #6914)
+  impacted released versions: none
+  impacted development branches:
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in:
+  found by: Roux, Melquiond
+  exploit:
+  GH issue number: #9925
+  risk:
+
   component: "native" conversion machine (translation to OCaml which compiles to native code)
   summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
   introduced: V8.5
@@ -207,6 +219,15 @@ Conversion machines
   GH issue number: ?
   risk: 
 
+  component: primitive projections, native_compute
+  summary: stuck primitive projections computed incorrectly by native_compute
+  introduced: 1 Jun 2018, e1e7888a, ppedrot
+  impacted released versions: 8.9.0
+  impacted coqchk versions: none
+  found by: maximedenes exploiting bug #9684
+  exploit: test-suite/bugs/closed/bug_9684.v
+  GH issue number: #9684
+
 Conflicts with axioms in library
 
   component: library of real numbers
diff --git a/dev/incdir_dune b/dev/incdir_dune
index 9d0fee1fa2..9ba31167b9 100644
--- a/dev/incdir_dune
+++ b/dev/incdir_dune
@@ -1,16 +1,17 @@
 #cd".";;
-#directory "_build/default/lib/.lib.objs/";;
-#directory "_build/default/clib/.clib.objs/";;
-#directory "_build/default/kernel/.kernel.objs/";;
-#directory "_build/default/library/.library.objs/";;
-#directory "_build/default/engine/.engine.objs/";;
-#directory "_build/default/pretyping/.pretyping.objs/";;
-#directory "_build/default/interp/.interp.objs/";;
-#directory "_build/default/parsing/.parsing.objs/";;
-#directory "_build/default/gramlib/.gramlib.objs/";;
-#directory "_build/default/proofs/.proofs.objs/";;
-#directory "_build/default/tactics/.tactics.objs/";;
-#directory "_build/default/printing/.printing.objs/";;
-#directory "_build/default/vernac/.vernac.objs/";;
-#directory "_build/default/stm/.stm.objs/";;
-#directory "_build/default/toplevel/.toplevel.objs/";;
+#directory "_build/default/lib/.lib.objs/byte/";;
+#directory "_build/default/clib/.clib.objs/byte/";;
+#directory "_build/default/kernel/.kernel.objs/byte/";;
+#directory "_build/default/library/.library.objs/byte/";;
+#directory "_build/default/engine/.engine.objs/byte/";;
+#directory "_build/default/pretyping/.pretyping.objs/byte/";;
+#directory "_build/default/interp/.interp.objs/byte/";;
+#directory "_build/default/parsing/.parsing.objs/byte/";;
+#directory "_build/default/gramlib/.gramlib.objs/byte/";;
+#directory "_build/default/proofs/.proofs.objs/byte/";;
+#directory "_build/default/tactics/.tactics.objs/byte/";;
+#directory "_build/default/printing/.printing.objs/byte/";;
+#directory "_build/default/vernac/.vernac.objs/byte/";;
+#directory "_build/default/stm/.stm.objs/byte/";;
+#directory "_build/default/toplevel/.toplevel.objs/byte/";;
+#directory "_build/default/plugins/ltac/.ltac_plugin.objs/byte/";;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 74be300134..816316487c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -65,6 +65,7 @@ let get_current_context () =
   with Vernacstate.Proof_global.NoCurrentProof ->
     let env = Global.env() in
     Evd.from_env env, env
+  [@@ocaml.warning "-3"]
 
 (* term printers *)
 let envpp pp = let sigma,env = get_current_context () in pp env sigma