Library Coq.funind.FunInd
Require
Coq.extraction.Extraction
.
Declare
ML
Module
"recdef_plugin".