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

[JasonGross]

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.

[mattam82]

Right. This is certainly a priority.