6 files changed, 49 insertions, 7 deletions
diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
new file mode 100644
index 0000000000..a7ffde31fc
--- /dev/null
+++ b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  The warning raised when a trailing implicit is declared to be non maximally
+  inserted (with the command cmd:`Arguments <Arguments (implicits)>`) has been turned into an error.
+  This was deprecated since Coq 8.10.
+  (`#11368 <https://github.com/coq/coq/pull/11368>`_,
+  by SimonBoulier).
diff --git a/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst b/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst
new file mode 100644
index 0000000000..3e1f1e02a4
--- /dev/null
+++ b/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  Export of module ``RList`` in ``Ranalysis.v`` and ``Ranalysis_reg.v``. Module ``RList`` is still there but must be imported explicitly where required.
+  (`#11396 <https://github.com/coq/coq/pull/11396>`_,
+  by Michael Soegtrop).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index bdfdffeaad..510e271951 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1728,11 +1728,11 @@ Declaring Implicit Arguments
    To know which are the implicit arguments of an object, use the
    command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`).
 
-.. warn:: Argument number @num is a trailing implicit so must be maximal.
+.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ].
 
    For instance in
 
-   .. coqtop:: all warn
+   .. coqtop:: all fail
 
       Arguments prod _ [_].
 
diff --git a/doc/stdlib/dune b/doc/stdlib/dune
index 7fe2493fbf..828caecabc 100644
--- a/doc/stdlib/dune
+++ b/doc/stdlib/dune
@@ -5,7 +5,8 @@
  (deps
    make-library-index index-list.html.template hidden-files
    (source_tree %{project_root}/theories)
-   (source_tree %{project_root}/plugins))
+   (source_tree %{project_root}/plugins)
+   (source_tree %{project_root}/user-contrib))
  (action
   (chdir %{project_root}
    ; On windows run will fail
@@ -17,6 +18,7 @@
    ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
    (source_tree %{project_root}/theories)
    (source_tree %{project_root}/plugins)
+   (source_tree %{project_root}/user-contrib)
    (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
    (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
    ; For .glob files, should be gone when Coq Dune is smarter.
@@ -24,7 +26,7 @@
  (action
   (progn
    (run mkdir -p html)
-   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)")
+   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)")
    (run mv html/index.html html/genindex.html)
    (with-stdout-to
      _index.html
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index ac611926b3..5e13214a1a 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -626,6 +626,31 @@ through the <tt>Require Import</tt> command.</p>
     plugins/ssr/ssrfun.v
   </dd>
 
+  <dt> <b>Ltac2</b>:
+    The Ltac2 tactic programming language
+  </dt>
+  <dd>
+    user-contrib/Ltac2/Ltac2.v
+    user-contrib/Ltac2/Array.v
+    user-contrib/Ltac2/Bool.v
+    user-contrib/Ltac2/Char.v
+    user-contrib/Ltac2/Constr.v
+    user-contrib/Ltac2/Control.v
+    user-contrib/Ltac2/Env.v
+    user-contrib/Ltac2/Fresh.v
+    user-contrib/Ltac2/Ident.v
+    user-contrib/Ltac2/Init.v
+    user-contrib/Ltac2/Int.v
+    user-contrib/Ltac2/List.v
+    user-contrib/Ltac2/Ltac1.v
+    user-contrib/Ltac2/Message.v
+    user-contrib/Ltac2/Notations.v
+    user-contrib/Ltac2/Option.v
+    user-contrib/Ltac2/Pattern.v
+    user-contrib/Ltac2/Std.v
+    user-contrib/Ltac2/String.v
+  </dd>
+
   <dt> <b>Unicode</b>:
     Unicode-based notations
   </dt>
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index bea6f24098..732f15b78a 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/usr/bin/env bash
 
 # Instantiate links to library files in index template
 
@@ -8,9 +8,14 @@ HIDDEN=$2
 cp -f $FILE.template tmp
 echo -n "Building file index-list.prehtml... "
 
-LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native`
+LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native`
 
 for k in $LIBDIRS; do
+    if [[ $k =~ "user-contrib" ]]; then
+        BASE_PREFIX=""
+    else
+        BASE_PREFIX="Coq."
+    fi
     d=`basename $k`
       ls $k | grep -q \.v'$'
       if [ $? = 0 ]; then
@@ -26,7 +31,7 @@ for k in $LIBDIRS; do
                     echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1
                 else
 		    p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'`
-		    sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
+		    sed -e "s:$k/$b.v:<a href=\"$BASE_PREFIX$p.$b.html\">$b</a>:g" tmp > tmp2
 		    mv -f tmp2 tmp
                 fi
 	    else