search

mattam82 / Coq-Equations

A function definition package for Coq
http://mattam82.github.io/Coq-Equations
GNU Lesser General Public License v2.1
223 stars 44 forks source link

Require Vector directly instead of through Bvector #589

Open andres-erbsen opened 6 months ago

andres-erbsen commented 6 months ago

I am investigating whether we could remove Bvector (vectors of bool) from stdlib. It looks like Equations was needlessly depending on it while only using the polymorphic Vector. I imagine this PR is an improvement regardless of whether Bvector is kept.

Tested with make && make test-suite.

proux01 commented 6 months ago

@mattam82 upstream PR merged, this can be merged at you convenience (doesn't make Coq CI error yet but still fixes a deprecation warning)