This release reflects the contents of the paper:
- Cyril Cohen and Kazuhiko Sakaguchi. A bargain for mergesorts — How to prove your mergesort correct and stable, almost for free. Proc. ACM Program. Lang. 9, ICFP, Article 236 (August 2025). [arXiv, doi]
It is compatible with Rocq/Coq 8.19 to 9.0, MathComp 2.3.0 to 2.4.0, and Paramcoq 1.1.3.