Emilio Jesús Gallego Arias (Jul 06 2020 at 11:17): Emilio Jesús Gallego Arias (Jul 06 2020 at 11:17):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?
Gaëtan Gilbert (Jul 06 2020 at 11:26):sounds fine
Thomas Letan (Jul 06 2020 at 13:28):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 :).
Emilio Jesús Gallego Arias (Jul 06 2020 at 14:06):Great, thanks @Thomas Letan , for now you have the lock until further notice
Emilio Jesús Gallego Arias (Jul 06 2020 at 14:06):I mean until you release it
Thomas Letan (Jul 06 2020 at 14:32):ack :)
Last updated: Apr 20 2024 at 08:02 UTC