Skip to content
GitLab

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

Merged 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.