(deprecation) warnings not shown when a tactic fails to apply

[hoheinzollern]

For example, a script like this:

#[deprecated(since = "0", note = "useless")]
Lemma one: False -> False.
Proof. auto. Qed.

Lemma two: False.
Proof. exact one.

would fail at exact one, but only the failure message is displayed in the interface, and the warning is not shown. This is the output by coqc:

File "./warning.v", line 8, characters 13-16:
Warning: Reference one is deprecated since 0. useless
[deprecated-reference-since-0,deprecated-since-0,deprecated-reference,deprecated,default]
File "./warning.v", line 8, characters 13-16:
Warning: Reference one is deprecated since 0. useless
[deprecated-reference-since-0,deprecated-since-0,deprecated-reference,deprecated,default]
File "./warning.v", line 8, characters 13-16:
Error:
The term "one" has type "False -> False" while it is expected to have type
 "False".

Ideally, I should be able to see the deprecation warning when a tactic fails to apply.

[hendriktews]

Thanks for the report. I can reproduce this with Coq 8.20 and current PG master.