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

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

• Shouldn't that be foo1 nat (1:=2)?
– Trebor
Aug 4 at 10:00
• This command seems more reasonable, but it still fails. Aug 4 at 11:24