package coq-mathcomp-field

  1. Overview
  2. Homepage
Compatibility package for rocq-mathcomp-field

Install

Dune Dependency

Authors

Maintainers

Sources

mathcomp-2.5.0.tar.gz
sha256=3db2f4b1b7f9f5a12d3d0c4ba4e325a26a77712074200319660c0e67e25679f1

Description

Published: 13 Nov 2025

Dependencies (1)

  1. rocq-mathcomp-field = version

Dev Dependencies

None

Used by (11)

  1. coq-infotheo >= "0.0.7" & < "0.1.1" | >= "0.5.1" & != "0.6.1" & != "0.7.5" & != "0.9.2"
  2. coq-libvalidsdp >= "1.1.1"
  3. coq-mathcomp-abel
  4. coq-mathcomp-analysis >= "0.3.13" & < "0.5.0" | >= "0.5.2" & != "0.5.4"
  5. coq-mathcomp-apery
  6. coq-mathcomp-cad
  7. coq-mathcomp-odd-order = "1.13.0"
  8. coq-mathcomp-real-closed >= "1.1.3"
  9. coq-mathcomp-sum-of-two-square >= "1.0.1"
  10. coq-monae >= "0.4.5"
  11. rocq-robot-rocq

Conflicts

None

Rocq

Interactive Theorem Prover