Snapshot of MetaCoq - accompanying material of the article:
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2020. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. Proc. ACM Program. Lang. 4, POPL, Article 8 (January 2020), 28 pages. https://doi.org/10.1145/3371076
See the README.md file for instructions on how to install and browse the sources.