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

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

3 files changed, 4 insertions, 4 deletions

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).