Repository navigation
The release updates coq-htt-core and core-htt to rocq-9.2/mathcomp-2.6.0.
It also contains the following new material:
- graph.v: Theory of partial graphs as Partial Commutative Monoids (PCMs). They key novelty is the use of PCM morphisms in verification, as explained in the ICFP 2025 paper by Grandury, Nanevski and Gryzlov
- schorr.v: Verification of the Schorr-Waite graph marking algorithm, from the same paper.
- union-find.v: Verification of union-find data structure from the same paper. Obsoletes the previous verification of union-find which didn't use PCM morphisms.