Apply suggestions from Hugo

Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>

2 files changed, 4 insertions, 35 deletions

diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
index dc4fdd48de..fd63980036 100644
--- a/dev/ci/user-overlays/11235-non-maximal-implicit.sh
+++ b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
@@ -6,35 +6,4 @@ if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]
     elpi_CI_REF=non_maximal_implicit
     elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi
 
-    # the following are also in 11368-trailing-implicit-error.sh
-    mathcomp_CI_REF=non_maximal_implicit
-    mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp
-
-    oddorder_CI_REF=non_maximal_implicit
-    oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order
-
-    stdlib2_CI_REF=non_maximal_implicit
-    stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2
-
-    coq_dpdgraph_CI_REF=non_maximal_implicit
-    coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph
-
-    vst_CI_REF=non_maximal_implicit
-    vst_CI_GITURL=https://github.com/SimonBoulier/VST
-
-    equations_CI_REF=non_maximal_implicit
-    equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations
-
-    mtac2_CI_REF=non_maximal_implicit
-    mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2
-
-    relation_algebra_CI_REF=non_maximal_implicit
-    relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra
-
-    fiat_parsers_CI_REF=non_maximal_implicit
-    fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat
-
-    Corn_CI_REF=non_maximal_implicit
-    Corn_CI_GITURL=https://github.com/SimonBoulier/corn
-
 fi
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 64864bb195..b3ebb4d8df 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1571,8 +1571,8 @@ implicitly applied to the implicit arguments it is waiting for: one
 says that the implicit argument is maximally inserted.
 
 Each implicit argument can be declared to be inserted maximally or non
-maximally. In Coq, maximally inserted implicits are written between curly braces
-"{ }" and non maximally inserted implicits are written in square brackets "[ ]".
+maximally. In Coq, maximally-inserted implicit arguments are written between curly braces
+"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]".
 
 .. seealso:: :flag:`Maximal Implicit Insertion`
 
@@ -1895,8 +1895,8 @@ Combining manual declaration and automatic declaration
 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
 When some arguments are manually specified implicit with binders in a definition
-and the automatic declaration mode in on, the manual implicits are added to the
-automatic ones.
+and the automatic declaration mode in on, the manual implicit arguments are added to the
+automatically declared ones.
 
 In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off,
 some trailing implicit arguments can be inferred to be non maximally inserted. In