package coq-mathcomp-ssreflect

  1. Overview
  2. Homepage
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)

  1. rocq-mathcomp-ssreflect = version
  2. coq-core

Dev Dependencies

None

Used by (41)

  1. coq-comp-dec-modal >= "1.2"
  2. coq-coqeal >= "2.0.0" & < "2.0.2" | >= "2.1.1"
  3. coq-coqeal-theory
  4. coq-coquelicot >= "2.1.1" & < "3.1.0" | >= "3.3.1" & < "3.4.1" | >= "3.4.4"
  5. coq-deriving >= "0.2.2"
  6. coq-dijkstra
  7. coq-disel-examples >= "2.3"
  8. coq-extructures >= "0.5.0"
  9. coq-fcsl-pcm >= "2.2.0"
  10. coq-fourcolor-reals >= "1.4.2"
  11. coq-gaia-numbers >= "2.0"
  12. coq-gaia-ordinals >= "2.0"
  13. coq-gaia-schutte >= "2.0"
  14. coq-gaia-stern >= "2.0"
  15. coq-gaia-theory-of-sets >= "2.0"
  16. coq-graph-theory >= "0.9.7"
  17. coq-hanoi
  18. coq-htt >= "2.2.1"
  19. coq-htt-core >= "2.2.1"
  20. coq-infotheo >= "0.7.0" & != "0.7.5" & < "0.9.2" | >= "0.9.6"
  21. coq-interval < "4.5.2" | >= "4.8.0"
  22. coq-mathcomp-bigenough != "1.0.2"
  23. coq-mathcomp-classical >= "1.14.0"
  24. coq-mathcomp-multinomials >= "2.4.0"
  25. coq-mathcomp-real-closed = "2.0.0" | >= "2.0.3"
  26. coq-mathcomp-tarjan >= "1.0.4"
  27. coq-mathcomp-zify >= "1.6.0+2.3+8.18"
  28. coq-monae >= "0.7.0"
  29. coq-msets-extra
  30. coq-num-analysis
  31. coq-plouffe >= "1.2.0"
  32. coq-quickchick >= "2.1.1"
  33. coq-regexp-brzozowski >= "1.2"
  34. coq-reglang >= "1.2.2"
  35. coq-ssprove >= "0.3.0"
  36. coq-trocq-hott-examples
  37. coq-type-infer
  38. coq-vellvm
  39. rocq-num-analysis-subset >= "2.1.0"
  40. rocq-robot-rocq
  41. rocq-vellvm

Conflicts

None

Rocq

Interactive Theorem Prover