The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
iMod and evar instantiation
See https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/acddfae5355a5e7540010c7ea6f423a892f9e887#note_17391: iMod ... as [$ ?] fails even though iMod ... as [H ?]; iFrame "H" works fine.
@jjourdan suggests it may be related to Coq lazily propagating instantiated evars, and adding a magic tactic that does the propagation in the right point of executing the iMod could help.