metacoq
metacoq copied to clipboard
[Feature Request] Please allow scripting `#[export] Typeclasses Opaque foo.` in the template monad
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.
Right. This is certainly a priority.