From Template Require Export TemplateMonad.Core.

Certifying extraction from Coq to L with time bounds