search

mit-plv / cross-crypto

Connecting computational and symbolic crypto models
MIT License
8 stars 19 forks source link

Fix for coq PR #13969 #26

Closed mattam82 closed 2 years ago

mattam82 commented 2 years ago

Do not merge, not backwards compatible a priori.

mattam82 commented 2 years ago

Please merge now

mattam82 commented 2 years ago

The removal of the eq_subrelation instance makes previous Coq versions fail as expected.

mattam82 commented 2 years ago

This is currently blocking Coq's CI.

JasonGross commented 2 years ago

@andres-erbsen Can we just drop compatibility with versions older than master?