Skip to content

Use a fully-qualified import for `matcomp.zify.srrZ`

https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/blob/v0.5/model/priority/gel.v#L4 This project imports ssrZ from mathcomp. It would be convenient if this could be changed to mathcomp.zify because otherwise it conflicts with coq-mathcomp-word. See also https://github.com/jasmin-lang/coqword/issues/15 and https://github.com/coq/opam-coq-archive/pull/2454#issuecomment-1406109451

(I'd make a PR, but I don't seem to have the rights to do this)

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information