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?
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)
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: Feb 09 2023 at 02:02 UTC