github.com/coq/opam-coq-archive
Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp
opam install coq-reglang.1.1.1