Package: wnpp Severity: wishlist Owner: Julien Puydt <jpu...@debian.org> X-Debbugs-Cc: debian-ocaml-ma...@lists.debian.org, jpu...@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
