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]). *)
  • $\begingroup$ Shouldn't that be foo1 nat (1:=2)? $\endgroup$
    – Trebor
    Aug 4 at 10:00
  • $\begingroup$ This command seems more reasonable, but it still fails. $\endgroup$ Aug 4 at 11:24

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

  • $\begingroup$ Thanks. I was using Coq 8.14 and my reference manual was for Coq 8.15. The command "Check foo1 nat (1:=2)." works. $\endgroup$ Aug 4 at 14:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.