Emilio Jesús Gallego Arias

Indeed, this is not really an error, but more like the map from names to locations we are using (toc for "table of contents") returns the latter location. To solve...

To fix the test for now I'd suggest renaming the hypothesis that is shadowing the lemma. But indeed, that's such a PITA.

I have been thinking about this, can you provide a more concrete example? I am wondering if that use case would be covered by just using multiple workspace roots (and...

Just another vote from people like me that need the quick and dirty fix of TLS.

> Yeah that's a bug. I don't suggest merging until we have a fix ready. It seems we need to split before doing the unescaping, I am not sure what...

It seems like `Fl_package_base.requires_deeply` is the function taking a large runtime.

That's a good idea, IMHO implementing #322 would be enough to implement this cleanly.

I am not sure Coq's API does expose this list tho.

Hi @patrick-nicodemus , this is indeed outdated, as the README was written before VsCoq 2 was released. Thanks for notification, we will amend ASAP.

Hi @dariusf , this is due to the memprof-limits interruption backend and a patch that wasn't applied to Coq upstream to make it safe w.r.t. this method. I will push...