github.com/coq/opam-coq-archive
Correctness of a tiny compiler for arithmetic expressions
opam install coq-mini-compiler.8.10.0