1 2 3 4 5 6
(library (name recdef_plugin) (public_name coq.plugins.recdef) (synopsis "Coq's functional induction plugin") (flags :standard -open Gramlib) (libraries coq.plugins.extraction))