blob: 42377f37f43448d47fce1763f05c13c46693a8bb (
plain)
1
2
3
4
5
6
7
|
(library
(name recdef_plugin)
(public_name coq-core.plugins.funind)
(synopsis "Coq's functional induction plugin")
(libraries coq-core.plugins.extraction))
(coq.pp (modules g_indfun))
|