Skip to content

Explicitly Require Coq Vector in vector.v (for coq/coq#18936)

Andres Erbsen requested to merge andres-erbsen/stdpp:require-vector into master

For https://github.com/coq/coq/pull/18936

I think previously stdpp vector.v pulled in stdlib Vector.v through NArith, Ndigits, and ByteVector.

Edited by Andres Erbsen

Merge request reports