Skip to content

Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512

Robbert Krebbers requested to merge robbert/coq_12512 into master

This MR provides an alternative to !165 (closed), but avoids the epose horribleness. Instead, it just spells out some proofs, which IMHO makes things easier to maintain.

Merge request reports