Maxime Dénès

> @maximedenes should I open a Coq issue about this (even though I don't know how to reproduce it without SerAPI)? If a bug is confirmed on the bug side,...

> Also, I'd like to do my part towards moving on from CoqIDE to something more flexible and modern. Not that CoqIDE is particularly bad, in fact it's surprisingly good,...

I think it is fairly obvious that reusing libobject for search is a hack. As for the need of dumping "what Coq knows to be in the .vo file", can...

Why not first remove the hack (which is what this PR does)? Then of course you can implement a mechanism that scales better (i.e. is more general) than using the...

The problem with discussing how we can do more *before* cleaning-up code is that it does not scale. If we do that for every feature we may want on every...

> Note that I didn't block the PR, I was just requesting a discussion, so still it is very puzzling to me that tag was removed unilaterally. Doesn't this label...

> How is the PR a net gain for you? It doesn't touch any libobject API, does it? I'm actually working at the declaremods level, where this PR removes an...

Anyway, I don't care much since I also can do with it, the point was just to illustrate. Having expressed my opinion and exhausted the time I could spend on...

Ok, so this patch is in fact not backward compatible. I'll prepare an overlay in the Coq PR.

I'll try to have a look at it