Julien Cretin

> I think you're being too hasty. That indicates that `term99` doesn't appear anywhere in the document (RHS or LHS). Ah you didn't mean in the refman. Indeed, there's a...

> but then `term99` is converted into `term10` somewhere else [Here](https://github.com/rocq-prover/rocq/blob/cfec7255070ee86fa58075ceb17fc08c73979aa8/doc/tools/docgram/common.edit_mlg#L2288), where we ask to SPLICE `term99`. I guess I can remove it and see what happens.

Ok, I've pushed a commit that fixes this `term99` issue. I also fixed the English text because that's not automatic.

> I did mean in the refman. Then my `grep` was about the refman. There is no occurrence of `term99` in the refman. My last commit adds it back. >...

Not splicing `term99` means we now get such an "empty" level: (This level is only used by a reserved notation in the prelude for the arrow.) We can't get rid...

I'd love to see `--config` supported by `cargo bloat`, but I tested this PR and it doesn't work for me. I'm still getting: ``` Warning: unused arguments left: ["--config=profile.release.lto=true", "--config=profile.release.opt-level=\"z\"",...

I agree forcing `checked` clauses to be on unsafe calls might be too restrictive (in particular in comparison with current practices of having unsafe comments on unsafe blocks). However this...

> `checked` can be attached to an unsafe block as long as the block containing single unsafe call (no restriction on how many safe calls are in it). Right. What...

> It's not allowed in this RFC due to exactly what you said Ok, so there's no trade-off. That's fine for me, I'm just noticing that some may find this...

What's the status on this feature request? I'm getting the following error on [this](https://github.com/lowRISC/opentitan/blob/1290004bc3ec4b5cf4b091b55e94ad199c68efe2/hw/top_earlgrey/data/top_earlgrey.hjson) file: ``` Error: "found a punctuator character when expecting a quoteless string" at line 1056 column...