Cyril Cohen
Cyril Cohen
Am I right that this is a backward compatible change? As long as client code does not start using `[in A]` and keep using `mem A`, they will not be...
> Is there some nix command that would allow me to quickly get to the context the CI will be in when trying to build graph-theory on top of this...
CC @gares note that `simpl never` does not have the same behavior as `nosimpl` when adding a definition on top of a `simpl never` one, we might go through the...
I will investigate `odd_order`
@gares, the problem we encountered is the one I mentioned for e.g. `pfactor`, except it occurs for a local definition, (for which there is no way to control the unfolding...
@ybertot @gares, Unfortunately, I think the consequence of this exploration is that this PR cannot be merged because it introduces a regression in the behaviour of symbols that are no...
> I have been trying to construct a minimal example, but I can't reproduce the problem in a few lines yet. I did it here https://github.com/coq/coq/issues/13428
> In the meantime shouldn't this PR be re-affected to milestone 1.13.0? I am afraid way later than 1.13 since, assuming someone fixes this for Coq 8.13, we would have...
@ejgallego and @gares should this be in 1.8.0 ?
Let's target 1.8.1 then! Thanks