Jan-Oliver Kaiser

> You could recover some efficiency by using all the bits in an int instead of just the lower 8 but since primitive ints are 63 bits it doesn't fit...

> Is there no issue with universes? What are you thinking of? Are you concerned that strictly unique goals might still influence other goals through their shared universe variables? I...

I added a test case that demonstrates the advantages of this change. I can also add the examples that actually led me here in the first place but they are...

Here's the full example. This approach is the only way I've found to insert a coq representation of a function's binder's name into the *surrounding* term (as opposed to the...

Wow. I am impressed and a little horrified. :) The number one disadvantage I see here is that the Ltac2 code needs to know about the shape of the terms...

I see. Our terms are not exactly huge so the cost of traversing could be OK. Still, I prefer my solution using volatile casts, I think. Either way, the change...

I've started using this code (only the first commit) and it does lead to some unintended consequences when non strictly unique goals rely on strictly-unique goals running first (or at...

Something is wrong with the code changes. I am getting a stack overflow in this branch but not on master with this example here: ``` Require Import Ltac2.Ltac1 Ltac2.Init Ltac2.Control...

I've lost most context on this change and just tried some more debugging on the reduced example only to realize that the stack overflow is due to the last commit....

The first commit has been used in production for several months with the only problem being that it is not always the right choice to re-order the independent group to...