Bug#1010650: ITP: mathcomp-real-closed -- Real closed fields for Mathematical Components

[Julien Puydt <jpuydt@debian.org>]

Package: wnpp
Severity: wishlist
Owner: Julien Puydt <jpuydt@debian.org>
X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org, jpuydt@debian.org

* Package name    : mathcomp-real-closed
  Version         : 1.1.2
  Upstream Author : Cyril Cohen and Assia Mahboubi
* URL             : https://github.com/math-comp/real-closed
* License         : CeCILL-B
  Programming Lang: Coq
  Description     : Real closed fields for Mathematical Components
 This library contains definitions and theorems about real closed fields
 for Mathematical Components. It includes a construction of the real
 and algebraic closure (with a proof of the fundamental theorem of
 algebra). The decidability of the first order theory of real closed
 field, through quantifier elimination is also established.

I plan to maintain it within the Debian OCaml Maintainers team, along with the
rest of the Coq-related packages.

Cheers,

J.Puydt