Erik Martin-Dorel

Anyway, feel free to close the issue if you think omitting `.. coq::` is not the "nominal syntax" and thereby Alectryon's behavior in this case should be ignored / kept...

@cpitclaudel > That's not really what happens; rather, Alectryon first reconstructs a reST file from the input, and to do so it needs to infer which depth to place the...

Hi @cpitclaudel > I think the best of both world could be to use this heuristic to produce warnings? Probably yes: if a warning (saying sth like "ambiguous code: you...

Hi @Bruno-366 (thanks @Zimmi48 thanks for the Cc!) I actually thought recently about a similar idea 🙂 (extending `docker-coq-action` or so with Alectryon support) when preparing this term a course...

Hi @Bruno-366, indeed; but as I just said in my previous comment (after the edit), you can use, from now on, this complete GHA workflow as a template for your...

OK! BTW regarding your earlier comment, @cpitclaudel: > I think a .deb package will take a long time to propagate if we want it in official sources, so it would...

OK! thank you @cpitclaudel for your feedback; for the record, there are several pip packages that already work in this way (I mean, not everything is installed by pip, only...

Hi @cpitclaudel, OK! > But doesn't company-coq-fold do what you want/need? We weren't aware of this one… it indeed helps for our use case, thanks :)

BTW, I guess this is related to this other issue: https://github.com/cpitclaudel/company-coq/issues/239

OK I see. Thanks for your comment. (I don't know if it'd be better to close this issue as wontfix, or add a `help wanted` label, or just keep it...