github.com/coq/opam-coq-archive
Implicit-complexity Coq library to prove that some programs are computable in polynomial time
opam install coq-cecoa.1.0.0