package coq-mathcomp-ssreflect
Compatibility package for rocq-mathcomp-ssreflect
Install
Dune Dependency
Authors
Maintainers
Sources
mathcomp-2.5.0.tar.gz
sha256=3db2f4b1b7f9f5a12d3d0c4ba4e325a26a77712074200319660c0e67e25679f1
Description
Published: 13 Nov 2025
Dependencies (2)
-
rocq-mathcomp-ssreflect
= version - coq-core
Dev Dependencies
None
Used by (37)
-
coq-comp-dec-modal
>= "1.2" -
coq-coqeal
>= "2.0.0" & < "2.0.2" - coq-coqeal-theory
-
coq-coquelicot
>= "2.1.1" & < "3.1.0" | >= "3.3.1" & < "3.4.1" | >= "3.4.4" -
coq-deriving
>= "0.2.2" - coq-dijkstra
-
coq-disel-examples
>= "2.3" -
coq-extructures
>= "0.5.0" -
coq-fcsl-pcm
>= "2.2.0" -
coq-fourcolor-reals
>= "1.4.2" -
coq-gaia-numbers
>= "2.0" -
coq-gaia-ordinals
>= "2.0" -
coq-gaia-schutte
>= "2.0" -
coq-gaia-stern
>= "2.0" -
coq-gaia-theory-of-sets
>= "2.0" -
coq-graph-theory
>= "0.9.7" - coq-hanoi
-
coq-infotheo
>= "0.7.0" & != "0.7.5" & < "0.9.2" | >= "0.9.6" -
coq-interval
< "4.5.2" | >= "4.8.0" -
coq-mathcomp-bigenough
!= "1.0.2" -
coq-mathcomp-classical
>= "1.14.0" -
coq-mathcomp-multinomials
>= "2.4.0" -
coq-mathcomp-real-closed
= "2.0.0" -
coq-mathcomp-tarjan
>= "1.0.4" -
coq-mathcomp-zify
>= "1.6.0+2.3+8.18" -
coq-monae
>= "0.7.0" - coq-msets-extra
- coq-num-analysis
-
coq-plouffe
>= "1.2.0" -
coq-quickchick
>= "1.1.0" -
coq-regexp-brzozowski
>= "1.2" -
coq-reglang
>= "1.2.2" -
coq-ssprove
>= "0.3.0" - coq-trocq-hott-examples
- coq-type-infer
- coq-vellvm
- rocq-vellvm
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page