Non-dependent implicit argument instantiation in Coq's reference manual does not work

Question

Consider the following definition

Definition foo1 (A : Type) {_ : A} := A.

I was wondering whether there is a way to instantiate the non-dependent implicit argument (the _ here) without using @, and I found that the "Explicit applications" section of https://coq.inria.fr/refman/language/extensions/implicit-arguments.html mentions that

To instantiate a non-dependent implicit argument, use the (natural := term) form of arg, where natural is the index of the implicit argument among all non-dependent arguments of the function (implicit or not, and starting from 1) and term is its corresponding explicit term.

However, the following commands fails

Check foo1 (1:=2).
Check foo1 nat (1:=2).

Moreover, it seems that Coq doesn't accept the grammer because even after adding a Fail before the commands, they still fail:

Fail Check foo1 (1:=2).
(* => Syntax error: ',' or ')' expected after [term level 200] (in [term]). *)
Fail Check foo1 nat (1:=2).
(* => Syntax error: ',' or ')' expected after [term level 200] (in [term]). *)

Answer 1

This is probably a Coq version mismatch. The default online reference manual is for the most recent Coq, which is 8.15.2 at the time of writing. In this version it works. I just tested 8.12.2 and I get the error you describe. You are encouraged to use a recent Coq version, but you can always check the reference manual for older versions from the menu on the lower left corner. For example, here is the refman for Coq 8.12.2.