The word "cbv" seems to be missing from the https://coq.github.io/doc/v8.12/refman/proof-engine/tactics.html#coq:tacn.cbv heading?
Thanks for noticing @Paolo G. Giarrusso. Can you open a PR adding the
cbv back? Or at least an issue, so that we keep track of this?
Filed as https://github.com/coq/coq/pull/12536.
Last updated: Oct 21 2021 at 20:02 UTC