Stream: Coq devs & plugin devs

Topic: Per definition typing_flags


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jul 06 2020 at 11:26):

sounds fine

view this post on Zulip 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 :).

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 14:06):

Great, thanks @Thomas Letan , for now you have the lock until further notice

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 14:06):

I mean until you release it

view this post on Zulip Thomas Letan (Jul 06 2020 at 14:32):

ack :)


Last updated: Oct 21 2021 at 20:02 UTC