Match does not understand matching on multiple values

[vzaliva]

To reproduce press C-A C-X RET and when prompted type nat, nat.
I expect it to generate match line this:

match _,_ with
 | O O => ...
 | S _, O => ...
 | O, S _ => ...
 | S _, S_ => ...
end.

I get the following error message instead:

company-coq-insert-match-construct: Toplevel input, characters 14-15:
> Show Match nat,nat.
>               ^
Syntax error: '.' expected after [vernac:command] (in [vernac_aux]).

[cpitclaudel]

I think it's a Coq-side problem; can you open a Coq bug report?
The issue is that Coq's Show Match command doesn't support pairs.

[vzaliva]

I have filed a bug https://coq.inria.fr/bugs/show_bug.cgi?id=5076
I let it up to you to decide whenever to keep this ticket open until it is fixed in Coq or close for now.

[Matafou]

This is not really a bug but a feature wish. The feature do support pairs, what is not supported is complex pattern matching (with notations). It is however a nice feature.