Advertisement for memprof-limits (reliable "fuel" and RAM usage limits); how to get started with its integration in Coq? Also, free discussion around asynchronous exceptions and all that if you want - gadmm
Notes
#12411: add a new late-local customization file.
News section: ok with the PR by Théo
Optional arguments for tactics (feature seems to be good for everyone). We might want a more uniform syntax to "unconfuse" with attributes.
At least we need delimiters:
@tactic (opts) could be an option but would require two parsing rules per tactic
tactic [opts] is a parsing nightmare (what if tactic takes an optional constr list after?)
tactic #[opts] is maybe dangerous if users already have defined notations for #[ c ] in constrs.
tactic @[opts] looked more innocent to us (@ is already a keyword as well)