package coq-mathcomp-ssreflect
Compatibility package for rocq-mathcomp-ssreflect
Install
Dune Dependency
Authors
Maintainers
Sources
mathcomp-2.4.0.tar.gz
sha256=6307218d7e434fb6ffc81b9275c673d3f7f1f4884ad59b904abd205c437021a0
Description
Published: 15 Apr 2025
Dependencies (2)
-
rocq-mathcomp-ssreflect
= version
- coq-core
Dev Dependencies
None
Used by (29)
-
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"
-
coq-deriving
>= "0.2.1"
- coq-dijkstra
-
coq-disel-examples
>= "2.3"
-
coq-extructures
>= "0.4.0"
-
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-hanoi
-
coq-infotheo
>= "0.7.0" & != "0.7.5"
-
coq-interval
< "4.5.2" | >= "4.8.0"
- coq-mathcomp-bigenough
-
coq-mathcomp-classical
>= "1.0.0"
-
coq-mathcomp-real-closed
= "2.0.0"
-
coq-mathcomp-tarjan
>= "1.0.2"
-
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-type-infer
- coq-vellvm
- rocq-vellvm
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page