Prosa does not compile with Coq 8.15.0 and mathcomp 1.14.0

There are some Ltac errors. See CI job #169764.

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