Yves Bertot

We should discuss with the Coq developers to see whether visibility can be handled directly at each command using attributes.

I followed the discussion from the start. Let's keep the idea of this interactive session, but this may not be the right place to discuss it.

Now that we plan to work on release 1.11, what is the status of this PR? is it better to move it to 1.12.

I don't understand why you mention only incompatibility with Coq 8.11, Nix CI for bundle 8.12+1.13, 8.13+1.13, 8.12+1.14, 8.13+1.14 are also failures. I only understood that this branch is premature...

I wish to wait until the next math-comp meeting to know what policy should maintained with respect to backward compatibility on the master branch. For now I am happy to...

Thanks, I will do as suggested, it may take a few days before I come back to it though.

Agreed, I will look into it (already discussed with Enrico).

This is included a pull request I just submitted.

I do not understand. `sorted_take` does not occur in the current master branch of math-comp. What is the commit that @proux01 mentions attached to?

thks, I did not pay enough attention.