Source: mathcomp-analysis Maintainer: Debian OCaml Maintainers Uploaders: Julien Puydt Section: ocaml Priority: optional Standards-Version: 4.6.2 Rules-Requires-Root: no Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libcoq-hierarchy-builder, libcoq-mathcomp-algebra, libcoq-mathcomp-field, libcoq-mathcomp-fingroup, libcoq-mathcomp-solvable, libcoq-mathcomp-ssreflect, libcoq-mathcomp-bigenough, libcoq-mathcomp-finmap, ocaml-dune Vcs-Browser: https://salsa.debian.org/ocaml-team/mathcomp-analysis Vcs-Git: https://salsa.debian.org/ocaml-team/mathcomp-analysis.git Homepage: https://github.com/math-comp/analysis Package: libcoq-mathcomp-analysis Architecture: any Depends: ${coq:Depends},${misc:Depends} Provides: ${coq:Provides} Description: analysis extension for Mathematical Components This package provides an extension for classical analysis for the Mathematical Components library. . The Mathematical Components library is a coherent repository of general-purpose formalized mathematical theories for the Coq proof assistant.