Should Template.TypingWf.on_option
be replaced by MCOption.on_Some_or_None
? (There's a (* TODO MOVE *)
)
I guess so, yes!
Urgh, I guess on_Some_or_None
returns a Prop
, we need one that returns a Type
here
https://github.com/MetaCoq/metacoq/pull/786
Jason Gross has marked this topic as resolved.
Last updated: May 31 2023 at 04:01 UTC