16 files changed, 68 insertions, 25 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3c427793e2..3c24ec28c4 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -47,9 +47,6 @@ before_script:
   - opam list
   - opam config list
 
-after_script:
-  - echo "The build completed normally (not a runner failure)."
-
 ################ GITLAB CACHING ######################
 # - use artifacts between jobs                       #
 ######################################################
@@ -662,5 +659,5 @@ plugin:plugin-tutorial:
 plugin:ci-quickchick:
   extends: .ci-template-flambda
 
-plugin:ci-relation-algebra:
+plugin:ci-relation_algebra:
   extends: .ci-template
diff --git a/META.coq.in b/META.coq.in
index ab142ccc43..ef5de8da2b 100644
--- a/META.coq.in
+++ b/META.coq.in
@@ -315,7 +315,7 @@ package "plugins" (
     archive(native)  = "micromega_plugin.cmx"
   )
 
-  package "newring" (
+  package "setoid_ring" (
 
     description = "Coq newring plugin"
     version     = "8.10"
@@ -351,7 +351,7 @@ package "plugins" (
     archive(native)  = "cc_plugin.cmx"
   )
 
-  package "ground" (
+  package "firstorder" (
 
     description = "Coq ground plugin"
     version     = "8.10"
@@ -387,7 +387,7 @@ package "plugins" (
     archive(native)  = "btauto_plugin.cmx"
   )
 
-  package "recdef" (
+  package "funind" (
 
     description = "Coq recdef plugin"
     version     = "8.10"
diff --git a/Makefile.ci b/Makefile.ci
index 000725b6b1..a244c17ef3 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -38,7 +38,7 @@ CI_TARGETS= \
     ci-mtac2 \
     ci-paramcoq \
     ci-quickchick \
-    ci-relation-algebra \
+    ci-relation_algebra \
     ci-sf \
     ci-simple-io \
     ci-stdlib2 \
diff --git a/Makefile.ide b/Makefile.ide
index 8f9088a04a..4cec7aa443 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -68,6 +68,7 @@ GTKBIN=$(shell pkg-config --variable=prefix gtk+-3.0)/bin
 GTKLIBS=$(shell pkg-config --variable=libdir gtk+-3.0)
 PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-2.0)/bin
 SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-3.0)/share
+ADWAITASHARE=$(shell ls -d /usr/local/Cellar/adwaita-icon-theme/*)/share
 
 ###########################################################################
 # CoqIde special targets
@@ -255,6 +256,9 @@ $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
 	$(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/styles/{styles.rng,classic.xml} $@/gtksourceview-3.0/styles/
 	cp -R "$(GTKSHARE)/"locale $@
 	cp -R "$(GTKSHARE)/"themes $@
+	$(MKDIR) $@/glib-2.0/schemas
+	glib-compile-schemas --targetdir=$@/glib-2.0/schemas "$(GTKSHARE)/"glib-2.0/schemas/
+	cp -R "$(ADWAITASHARE)/"icons $@
 
 $(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents
 	$(MKDIR) $@
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 6fcc64f77e..f09087b172 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -52,7 +52,7 @@ jobs:
   - script: |
       set -e
       brew update
-      brew install gnu-time opam pkg-config gtksourceview3
+      brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme
       pip3 install macpack
     displayName: 'Install system dependencies'
 
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-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/doc/changes.md b/dev/doc/changes.md
index 40c3c32e4f..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
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index b069cf27f4..a5e9023732 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -433,22 +433,26 @@ few other commands related to typeclasses.
 
 .. _TypeclassesTransparent:
 
-Typeclasses Transparent, Typclasses Opaque
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Typeclasses Transparent, Typeclasses Opaque
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. cmd:: Typeclasses Transparent {+ @ident}
 
    This command makes the identifiers transparent during typeclass
    resolution.
+   Shortcut for :n:`Hint Transparent {+ @ident } : typeclass_instances`.
 
 .. cmd:: Typeclasses Opaque {+ @ident}
 
-   Make the identifiers opaque for typeclass search. It is useful when some
-   constants prevent some unifications and make resolution fail. It is also
-   useful to declare constants which should never be unfolded during
-   proof-search, like fixpoints or anything which does not look like an
-   abbreviation. This can additionally speed up proof search as the typeclass
-   map can be indexed by such rigid constants (see
+   Make the identifiers opaque for typeclass search.
+   Shortcut for :n:`Hint Opaque {+ @ident } : typeclass_instances`.
+
+   It is useful when some constants prevent some unifications and make
+   resolution fail. It is also useful to declare constants which
+   should never be unfolded during proof-search, like fixpoints or
+   anything which does not look like an abbreviation. This can
+   additionally speed up proof search as the typeclass map can be
+   indexed by such rigid constants (see
    :ref:`thehintsdatabasesforautoandeauto`).
 
 By default, all constants and local variables are considered transparent. One
@@ -458,8 +462,6 @@ type, like:
 .. coqdoc::
    Definition relation A := A -> A -> Prop.
 
-This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
-
 
 Settings
 ~~~~~~~~
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 8346b72cb9..35231610fe 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -144,6 +144,10 @@ Here we describe only few of them.
 :CAMLFLAGS:
    can be used to specify additional flags to the |OCaml|
    compiler, like ``-bin-annot`` or ``-w``....
+:OCAMLWARN:
+   it contains a default of ``-warn-error +a-3``, useful to modify
+   this setting; beware this is not recommended for projects in
+   Coq's CI.
 :COQC, COQDEP, COQDOC:
    can be set in order to use alternative binaries
    (e.g. wrappers)
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index e6922408aa..8d9e99b9d5 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4724,6 +4724,12 @@ Non-logical tactics
    from the shelf into focus, by appending them to the end of the current
    list of focused goals.
 
+.. tacn:: unshelve @tactic
+   :name: unshelve
+
+   Performs :n:`@tactic`, then unshelves existential variables added to the
+   shelf by the execution of :n:`@tactic`, prepending them to the current goal.
+
 .. tacn:: give_up
    :name: give_up
 
diff --git a/lib/envars.ml b/lib/envars.ml
index 0f4670688b..af8e45b137 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -178,6 +178,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs =
   fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
   fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
   fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags;
+  fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3";
   fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name
     (if Coq_config.has_natdynlink then "true" else "false");
   fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs)
diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
index 002eb28eea..6ccf15df29 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -1,5 +1,5 @@
 (library
  (name recdef_plugin)
- (public_name coq.plugins.recdef)
+ (public_name coq.plugins.funind)
  (synopsis "Coq's functional induction plugin")
  (libraries coq.plugins.extraction))
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 78a3f7c63a..4ee4aae36c 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -49,16 +49,15 @@ TO_SED_IN_BOTH=(
     -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out
     -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators
     -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it
+    -e s'/[0-9]//g' # sometimes the time is under 1 minute, sometimes it's over 1 minute, so we want to remove/normalize both instances; see https://github.com/coq/coq/issues/5675#issuecomment-487378622
 )
 
 TO_SED_IN_PER_FILE=(
-    -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
     -e s'/  */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start
     -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign
 )
 
 TO_SED_IN_PER_LINE=(
-    -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
     -e s'/  */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
     )
 
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 51e0300182..2ec55d1bd0 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -38,6 +38,7 @@ DOCDIR            := $(COQMF_DOCDIR)
 OCAMLFIND         := $(COQMF_OCAMLFIND)
 CAMLFLAGS         := $(COQMF_CAMLFLAGS)
 HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
+OCAMLWARN         := $(COQMF_WARN)
 
 @CONF_FILE@: @PROJECT_FILE@
 	@COQ_MAKEFILE_INVOCATION@
@@ -190,9 +191,9 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@
 COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
 
 CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
-
 # ocamldoc fails with unknown argument otherwise
-CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
+CAMLFLAGS+=$(OCAMLWARN)
 
 ifneq (,$(TIMING))
 TIMING_ARG=-time