Merge PR #11368: Turn trailing implicit warning into an error

Ack-by: Zimmi48
Reviewed-by: herbelin
Ack-by: maximedenes

10 files changed, 53 insertions, 16 deletions

diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
new file mode 100644
index 0000000000..a125337dd9
--- /dev/null
+++ b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
@@ -0,0 +1,33 @@
+if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then
+
+    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/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/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/interp/impargs.ml b/interp/impargs.ml
index df28b32f81..e2c732809a 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -646,11 +646,9 @@ let maybe_declare_manual_implicits local ref ?enriching l =
   if List.exists (fun x -> x.CAst.v <> None) l then
     declare_manual_implicits local ref ?enriching l
 
-(* TODO: either turn these warnings on and document them, or handle these cases sensibly *)
 
-let warn_set_maximal_deprecated =
-  CWarnings.create ~name:"set-maximal-deprecated" ~category:"deprecated"
-    (fun i -> strbrk ("Argument number " ^ string_of_int i ^ " is a trailing implicit so must be maximal"))
+let msg_trailing_implicit id =
+  user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]."))
 
 type implicit_kind = Implicit | MaximallyImplicit | NotImplicit
 
@@ -662,7 +660,7 @@ let compute_implicit_statuses autoimps l =
     | Name id :: autoimps, Implicit :: manualimps ->
        let imps' = aux (i+1) (autoimps, manualimps) in
        let max = set_maximality imps' false in
-       if max then warn_set_maximal_deprecated i;
+       if max then msg_trailing_implicit id;
        Some (ExplByName id, Manual, (max, true)) :: imps'
     | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
        user_err ~hdr:"set_implicits"
diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v
index ff08bdc6bb..52cc34beb3 100644
--- a/test-suite/bugs/closed/bug_2729.v
+++ b/test-suite/bugs/closed/bug_2729.v
@@ -82,7 +82,7 @@ Inductive SequenceBase (pu : PatchUniverse)
                      (p : pu_type from mid)
                      (qs : SequenceBase pu mid to),
               SequenceBase pu from to.
-Arguments Nil [pu cxt].
+Arguments Nil {pu cxt}.
 Arguments Cons [pu from mid to].
 
 Program Fixpoint insertBase {pu : PatchUniverse}
diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v
index 298a07c1c4..7022987096 100644
--- a/test-suite/complexity/injection.v
+++ b/test-suite/complexity/injection.v
@@ -47,7 +47,7 @@ Parameter mkJoinmap :   forall (key: Type) (t: Type) (j: joinable t),
 joinmap key j.
 
 Parameter ADMIT: forall p: Prop, p.
-Arguments ADMIT [p].
+Arguments ADMIT {p}.
 
 Module Share.
 Parameter jb : joinable bool.
diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index d293dc0533..048fb3b027 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -65,7 +65,7 @@ Proof. by []. Qed.
 
 Lemma eqP T : Equality.axiom (@eq_op T).
 Proof. by case: T => ? []. Qed.
-Arguments eqP [T x y].
+Arguments eqP {T x y}.
 
 Delimit Scope eq_scope with EQ.
 Open Scope eq_scope.
@@ -345,7 +345,7 @@ Proof. by []. Qed.
 
 End SubEqType.
 
-Arguments val_eqP [T P sT x y].
+Arguments val_eqP {T P sT x y}.
 Prenex Implicits val_eqP.
 
 Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T)
@@ -386,7 +386,7 @@ Qed.
 Canonical nat_eqMixin := EqMixin eqnP.
 Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
 
-Arguments eqnP [x y].
+Arguments eqnP {x y}.
 Prenex Implicits eqnP.
 
 Coercion nat_of_bool (b : bool) := if b then 1 else 0.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index d17b266690..4b2d4457bf 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -71,7 +71,7 @@ CoInductive LList (A : Set) : Set :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Inductive Finite (A : Set) : LList A -> Prop :=
   | Finite_LNil : Finite LNil
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 1dbeaf3e1f..8297f54641 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type :=
   | in_first : forall e, in_extension r (add_rule r e)
   | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e).
 
-Arguments NL [I].
+Arguments NL {I}.
 
 Inductive super_extension (I : Set) (e : extension I) :
 extension I -> Type :=
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 4fac798f76..15672eab7c 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -994,7 +994,7 @@ Qed.
 
 
 Arguments Vector.cons [A] _ [n].
-Arguments Vector.nil [A].
+Arguments Vector.nil {A}.
 Arguments Vector.hd [A n].
 Arguments Vector.tl [A n].
 
@@ -1161,7 +1161,7 @@ infiniteproof map_iterate'.
 Qed.
 
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
                                LNil <> (LCons a l).