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