github.com/coq/opam-coq-archive
Implementation and verification of an erasure procedure for Coq
opam install coq-metacoq-erasure.1.0~beta1+8.12