not sure we need a coq call to decide this
is there any reason not to merge https://github.com/coq/coq/pull/14621 now?
Looks very cool! Maybe we merge and let it evolve with the practice?
About a few questions:
needs: triage
: that looks good to have itOn a related note, I would split the inductive types
label into inductive types
and fixpoint
because it is often unrelated. I find that reduction strategies
referring to Strategy
is too narrow. Maybe could it be renamed to control of reduction
, referring to Strategy, Opaque, Tranparent, ... or generalized to include the reduction tactics (simpl, cbn, ...). Something about coqtop and coqc is missing (that could possibly put in Tools
but Tools
, currently starting with coqdoc
is too narrow; so it could be Command line tools: coqtop, coqc, coqdoc, ...
though I think I would put coqdoc and coq_makefile in their own category.
For the labels, feel free to do such changes directly.
For the PR, feel free to push a commit adding the "if any" if you think they are necessary. I didn't because none of the text boxes are compulsory.
I think indeed it doesn't need a Coq Call discussion probably.
merged
reminder that https://github.com/coq/coq/issues/new still produces a non-template issue (it is also linked as "open a blank issue" in a de-emphasized position from the template chooser)
This is still listed as a discussion point on https://github.com/coq/coq/wiki/Coq-Call-2024-03-19, but it could be removed now, right?
dnoe
Last updated: Oct 13 2024 at 01:02 UTC