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 13 2024 at 01:02 UTC