coq-mathcomp-experimental-reals.opam

opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
version: "dev"

homepage: "https://github.com/math-comp/analysis"
dev-repo: "git+https://github.com/math-comp/analysis.git"
bug-reports: "https://github.com/math-comp/analysis/issues"
license: "CECILL-C"

synopsis: "A library for alternative real numbers for mathematical components"
description: """
This package contains an experiment along real numbers
made at the beginning of the MathComp-Analysis library
(which now offers the coq-mathcomp-reals package).

Beware that this still contains a few Admitted."""

build: [make "-C" "experimental_reals" "-j%{jobs}%"]
install: [make "-C" "experimental_reals" "install"]
depends: [
  "coq-mathcomp-reals" { = version}
  "coq-mathcomp-bigenough" { (>= "1.0.0") }
]

tags: [
  "category:Mathematics/Real Numbers"
  "keyword:real numbers"
  "keyword:reals"
  "logpath:mathcomp.experimental_reals"
]
authors: [
  "Reynald Affeldt"
  "Alessandro Bruni"
  "Yves Bertot"
  "Cyril Cohen"
  "Marie Kerjean"
  "Assia Mahboubi"
  "Damien Rouhling"
  "Pierre Roux"
  "Kazuhiko Sakaguchi"
  "Zachary Stone"
  "Pierre-Yves Strub"
  "Laurent Théry"
]