I used the ml tag because there is no coq tag ):.
[Comment removed by author]
Not only is Coq written in OCaml, but Coq itself is “ML on steroids”:
Yes of course, this is why I’ve finally chosen it (:
I tag those with programming and math since that seems most accurate.
It makes sense, especially if the article focus on the “extraction” face of Coq (at least, it justifies better the programming tag).