github.com/coq/opam-coq-archive
An example Coq plugin, defining a tactic to get the constructors of an inductive type in a list
opam install coq-constructors.1.0.0