metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard

[Feature Request] Please allow scripting `#[export] Typeclasses Opaque foo.` in the template monad

Open JasonGross opened this issue 2 years ago • 1 comments

Without the ability to script this, the typeclass resolution in my Gallina quotation branch is very, very slow (like, 40 seconds for a single trivial goal slow), unless I manually emit hundreds of #[export] Typeclasses Opaque lines.

JasonGross avatar Mar 01 '23 05:03 JasonGross

Right. This is certainly a priority.

mattam82 avatar Jan 25 '24 17:01 mattam82