Enrico Tassi (Nov 26 2021 at 17:53): Enrico Tassi (Nov 26 2021 at 17:53):Can someone explain what the META file in the template coq sub folder is for? Also, there are two mlpack files (two plugins). What are they exactly? Why only one is on the META file?
Matthieu Sozeau (Nov 30 2021 at 10:10):I don't think we updated the META file in a while. There are two plugins indeed: the "light" template-coq reification/quotation stuff used to run MetaCoq live in Coq and the extractable version that is used for ocaml plugins (e.g. the implementations of MetaCoq Erase and MetaCoq Check link to that)
Enrico Tassi (Nov 30 2021 at 14:05):Thanks, I found that info in a comment at some point. I'll open a PR soon, let's see if my changes to the META file are OK
Last updated: Apr 16 2024 at 15:02 UTC