Coq-Equations icon indicating copy to clipboard operation
Coq-Equations copied to clipboard

Published 20 hours ago • verified publisher icon mattam82

Vernacular `Derive` conflicts with Rocq Derive feature

Open andres-erbsen opened this issue 5 months ago • 0 comments

Vernacular Derive conflicts with Rocq Derive feature. This means that using Derive in stdlib makes Equations build fail.

See also:

  • https://github.com/mattam82/Coq-Equations/pull/645

andres-erbsen avatar Jun 14 '25 23:06 andres-erbsen