Anonymous implicit generalization is not recognized

[Tuplanolla]

Versions

Coq 8.15.0

Coqtail 1.6.2

Vim 8.2

Equations 1.3

Python 3.7.4

Description

Unnamed parameters introduced by implicit generalization are highlighted as if they were named parameters without explicit type signatures. Looking at Coq's own theories/Classes/EquivDec.v demonstrates both sides of this issue.

Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
  match x with
    | left H => @right _ _ H
    | right H => @left _ _ H
  end.

Definition equiv_decb `{EqDec A} (x y : A) : bool :=
  if x == y then true else false.

The implicit parameters of swap_sumbool and equiv_decb are A B : Type and H : EqDec A respectively.

[whonore]

Are you saying you'd expect the A in EqDec A to be highlighted differently from EqDec and A, B in swap_sumbool? Coqtail's highlighting currently doesn't make much (any?) effort to distinguish between parameters and arguments and just calls them all Identifiers, but I'd welcome any PRs improving the situation. Possibly related: #165.

[Tuplanolla]

I would expect A, B and H to be Identifiers and Type and EqDec A to be plain terms, just like x and y are Identifiers and A is a plain term.

[whonore]

Oh ok, I think I understand. So if there's no explicit :, everything in {} should be treated as if it comes before a : (Identifier), and within <backtick>{} everything should be treated as coming after a : (coqBinderTypeCurly, which has no special highlighting currently).