github.com/coq/opam-coq-archive
ML-like recursive definitions
opam install coq-recursive-definition.8.6.0