Posted on https://github.com/coq/coq/issues/4712#issuecomment-1175466710 which seems most related.
the Definition A should be before the Fail otherwise it doesn't test quite the right thing
Fair enough, fixed here and on github.
Last updated: Feb 04 2023 at 21:02 UTC