Emilio Jesús Gallego Arias

Installing into the opam switch will make the default paths work, however plugins will become out of date the moment you rebuild and the interface changes [so you need to...

For these kind of questions Gitter may be the perfect spot.

Indeed `TypeOf` only admits identifiers at the moment; hopefully will take care of that in the new query language.

You could give it a go, however there is the issue of choice of input representation that we still didn't handle at all.

@palmskog I need to look deeper into this but surely a bug in Coq. When I first tweaked the parsing API to expose locs we found many bugs, basically the...

> I don't know how to reproduce it without SerAPI You could likely try to do it from `Drop.`.

Umm, do you have a regular self-contained simple example using just `Notation`, such that we can compare the actual output with the correct output?

8.12 changed a few things on this, let's reevaluate on the 0.12 branch is ready.

Ack, as discussed on Gitter there are several alternatives; I will prepare a proposal to expose internalization next week, let's see if that's enough for your use case.

Sure it should be possible to do so; I will prepare a patch later this week, or you could try to give it a go, if you look at the...