Coq question. compile errors. [file-no-extension,filesystem] and grammar entry "ident" permitted "_"

Question

We are very very beginner for coq. The following is code in Basic.v

1 Set Implicit Arguments.
2
3 (* Pretty-print for if-then-else expressions on informative types *)
4
5 Notation "'If' c1 'then' c2 'else' c3" :=
6   match c1 with
7   | left _ => c2
8   | right _ => c3
9   end (at level 200).
10
11  Notation "'IF' c1 'THEN' c2 'ELSE' c3" :=
12  (IF c1 then c2 else c3)(at level 200, v ident).
13
14  Definition IFEXTHENELSE (A : Set) (P1 P2 : A -> Prop) 
15 (P3 : Prop) := (exists2 x : A, P1 x & P2 x) \/ ~ (exists x : A, P1 x) /\ P3.
16
17 Notation "'IFEX' v | c1 'THEN' c2 'ELSE' c3" :=
18 (IFEXTHENELSE (fun v => c1) (fun v => c2) c3) (at level 200, v ident).

We met the following warning during compile of some existing files.

coqc -noglob  -q  -R . K Lib\Basic
Warning: File ".\Lib\Basic" has been implicitly expanded to ".\Lib\Basic.v"
[file-no-extension,filesystem]
File ".\Lib\Basic.v", line 11, characters 0-91:
Warning: grammar entry "ident" permitted "_" in addition to proper
identifiers; this use is deprecated and its meaning will change in the
future; use "name" instead. [deprecated-ident-entry,deprecated]
File ".\Lib\Basic.v", line 11, characters 0-91:
Error: v is unbound in the notation.

There are two warnings and one error.

1. [file-no-extension,filesystem] .
   If you can explain, could you please let us know the meaning of the warning?

2. Warning: grammar entry "ident" permitted "_" We cannot understand the meaning of the above grammer warning. could you please inform us the meaning?

3. error. Unbounded.

Thank you very much in advance

Answer 1

1. You should use Lib\Basic.v instead of Lib\Basic when compiling the file. This will prevent the first warning.

2. In the first notation, you declared an identifier v even though no such v appears in the notation. Just remove the declaration and the error will go away:

    Notation "'IF' c1 'THEN' c2 'ELSE' c3" :=
      (IF c1 then c2 else c3)(at level 200).
   

3. Finally, in the last notation you declared v as an identifier. Coq is just warning you that the behavior of identifiers is going to change. Right now, you can write something like

    IFEX _ | True THEN False ELSE TRUE
   

   where the _ indicates that the bound name is not used in the arguments of the if. If you want this behavior, you should instead write

    Notation "'IFEX' v | c1 'THEN' c2 'ELSE' c3" :=
     (IFEXTHENELSE (fun v => c1) (fun v => c2) c3) (at level 200, v name).
   

   where v ident was replaced by v name. This will still work in future versions of Coq.