coq-mathcomp-real-closed

Mathematical Components Library on real closed fields

opam install coq-mathcomp-real-closed.1.1.2
homepage
https://github.com/math-comp/real-closed
license
CECILL-B
bugs tracker
https://github.com/math-comp/real-closed/issues
dependencies
"coq" {(>= "8.10" & < "8.14~") | (= "dev")} "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.13~") | (= "dev")} "coq-mathcomp-algebra" {(>= "1.12.0" & < "1.13~") | (= "dev")} "coq-mathcomp-field" {(>= "1.12.0" & < "1.13~") | (= "dev")} "coq-mathcomp-bigenough" {>= "1.0.0"}
source
https://github.com/math-comp/real-closed/archive/1.1.2.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.1.1.2