Stream: Coq devs & plugin devs

Topic: Reference manual


view this post on Zulip Paolo Giarrusso (Jun 17 2020 at 00:41):

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?

view this post on Zulip Théo Zimmermann (Jun 17 2020 at 07:36):

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?

view this post on Zulip Paolo Giarrusso (Jun 17 2020 at 15:55):

Filed as https://github.com/coq/coq/pull/12536.


Last updated: Oct 21 2021 at 20:02 UTC