You are viewing the
staging branch
of the website @
b4332b8
, not the
live version
.
Dismiss
Search Rocq packages
Standard Library
Learn
Platform
Packages
Community
Consortium
News
Search Rocq packages
Learn
Platform
Packages
Community
Consortium
News
Standard Library
Get started
package
coq-mathcomp-reals
latest (1.16.0)
1.16.0
1.15.0
1.14.0
1.13.0
1.12.0
1.11.0
1.10.0
1.9.0
1.8.0
1.7.0
search
Overview
Homepage
You can search for identifiers within the package.
in-package search v0.2.0
Compatibility package for rocq-mathcomp-reals
Install
Dune Dependency
github.com
Edit opam file
Versions (10)
Authors
R
Reynald Affeldt
A
Alessandro Bruni
Y
Yves Bertot
C
Cyril Cohen
M
Marie Kerjean
A
Assia Mahboubi
D
Damien Rouhling
P
Pierre Roux
K
Kazuhiko Sakaguchi
Z
Zachary Stone
P
Pierre-Yves Strub
L
Laurent Théry
Maintainers
R
Reynald Affeldt <reynald.affeldt@aist.go.jp>
Description
Published:
16 Mar 2026
Dependencies (1)
rocq-mathcomp-reals
= version
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page
Description
Dependencies (1)
Dev Dependencies
Used by
Conflicts