Hi @Thomas Letan , @Gaëtan Gilbert ,
this thread is to sync on https://github.com/coq/coq/pull/12586 and https://github.com/coq/coq/pull/12539 .
The two first commits on 12586 are orthogonal to 12539 , but as Gaëtan don't want that API to go in unused [understandably] , I did a 3rd commit trying to add some basic support, but is still not finished. I guess [with https://github.com/coq/coq/pull/9004 ] there is some design space on how to interpret things, for example I've opted for the attributes to work over the full typing flags; I dunno. WDYT guys?
I will try to have a look at this asap. Thanks for providing a first draft of implementation, it will be easier for me to understand how your PR is supposed to work :).
Great, thanks @Thomas Letan , for now you have the lock until further notice
I mean until you release it
Last updated: Oct 21 2021 at 20:02 UTC