Pattern matching: warn unused parameter?

Using Rocq
1

Day 1, I defined a type foo and a function bar:

Variant foo := A | B.

Definition bar (x : foo) : bool :=
  match x with
  | A => true
  | B => false
  end.

Day 2, I modified type foo:

Variant foo := A | C | D.

but forgot to update bar accordingly. However, bar still compiles—it treated B as a wildcard rather than constructor.

Is there an equivalent to “unused parameter” warning for Coq? If no, is it worth adding such warning and suggest replacing pattern B with _?

2

See https://github.com/coq/coq/pull/12768