Emilio Jesús Gallego Arias

I think redirect is not working properly in 8.7, see coq/coq#6130 . It should be easy to fix.

Note that @matafou has mentioned that `infoH` is broken for inversion, so results won't be accurate I think.

Unfortunately the issue is deeper than that (and it has to do with the phase `as` is interpreted wrt the context `infoH` looks at): ``` Inductive a : nat ->...

In fact company-coq could almost provide a reasonable basis for the current inversion `as` clause by inspecting the constructors, unfortunately the `injection` step puts a bit of burden on the...

@vzaliva Coq grammar is already accessible from the vernacular or from alternative toplevels such as SerAPI; a different issue is to build a tool that can autocomplete using it.

Does `Print Grammar vernac.` work? The "full" full grammar is not really exported by `Print Grammar` due to the structure of the internal Entry printer, but we could workaround that...

@vzaliva we should make `Print Grammar printable` work, this is what I meant about the hard-coded entry table.

> @ejgallego I can take a look at making Print Grammar work for all non-terminals. It looks like a nice small problem for a newbie like me to get into...

A different approach is to use `Entry.obj` to cast a top-level entry to its representation and analyze the particular grammar entry. For that you want to look at the `Gramext`...

@vzaliva sure feel free to move this elsewhere; if you go for the first approach the first milestone is to get Coq to print a message every time a new...