Bug#1014955: ITP: coq-corn -- Coq Constructive Repository at Nijmegen

[Julien Puydt <jpuydt@debian.org>]

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

* Package name    : coq-corn
  Version         : 8.13.0
  Upstream Author : Bas Spitters (maintainer)
* URL             : https://github.com/coq-community/corn
* License         : GPL-2, GPL-2+ and Expat
  Programming Lang: Coq
  Description     : Coq Constructive Repository at Nijmegen
 This library provides different theories for Coq:
  - an algebraic hierarchy with an axiomatic formalization
 of the most common algebraic structures, like setoids,
 monoids, groups, rings, fields, ordered fields, rings of
 polynomials and real and complex numbers;
  - a construction of the real numbers satisfying the above
 axiomatic description;
  - a proof of the fundamental theorem of algebra;
  - a collection of elementary results on real analysis
  including continuity, differentiability, integration,
  Taylor's theorems and the fundamental theorem of calculus;
  - tools for exact real computations like real numbers,
  functions, integrals, graph of functions and differential
  equations.
 .
 Coq is a proof assistant for higher-order logic.


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

Cheers,

J.Puydt