Matthieu Sozeau

Ah I see, its probably better in a separate list indeed. I'm using the coqdoc frontend with no option to declare them there, AFAIK.

I fixed the closed issues counts where I could

Rather than a CMap.t you should probably use a map from global references to handle all of the inductives/constructors/constants/variables at once, no? I'm also curious what the "inversion of libobject"...

Yep, sounds right.

I don’t have many tricks, indeed Emacs support is lacking. One can use _ to not give a term directly and then try to figure out which obligation corresponds to...

In the current master branch, one can use `Equations? foo` to get goals instead of obligations corresponding to the holes of the program. This ressembles Agda-style interaction a little bit...

Most of the time, it follows textual order, but not always. It's only a poor man's solution :)

It might help to use `Set Equations Debug` to trace where/why covering fails.

Could you make a smaller example without CpdtTactics?

It is LGPL-2.1, I don't know why the or-later popped up in the opam package.