Emilio Jesús Gallego Arias

> Why not to do it as a primitive instead. Then it could also take an `int` argument, as "Show". What's a primitive?

> I think we meant in ocaml using a `TACTIC EXTEND`. That could work, however IMHO I think we could add something more flexible that could allow for a more...

Indeed, while I don't oppose to this as it is pretty harmless in terms of code-base, I wonder about what methodology we are following here. From my point of view...

Thanks for the comments @herbelin ; as I said I don't oppose this. I'm glad you found this usable, indeed that answers my question at least if it works for...

> The most conservative would be mutual definitions since it would preserve the old name `add_mutual_definitions`, so I'm leaning for it. Sounds good @herbelin , I have no strong opinion,...

@SkySkimmer the required independent fix is that coqdep doesn't properly resolve the findlib paths in windows, due to drive letters not playing nice with the relativization path. See Windows CI...

Other than the windows build problem, I think this is looking good. It would be still good to fix the problem with plugins that extend the grammar needing to be...

Ideally we could reimplement `Fl_dynload.load_packages` ourselves, it is not so hard, and add the corresponding grammar hooks for every plugin loaded.

Let's restore parsing of the old Declare ML Form, as not to force the overlays so much. This will however delay fixing the problem about some findlib names not being...

@coqbot run full CI