1 2 3 4 5
(library (name recdef_plugin) (public_name coq.plugins.funind) (synopsis "Coq's functional induction plugin") (libraries coq.plugins.extraction))