diff options
Diffstat (limited to 'debian/control')
| -rw-r--r-- | debian/control | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/debian/control b/debian/control new file mode 100644 index 0000000..db9364a --- /dev/null +++ b/debian/control @@ -0,0 +1,42 @@ +Source: ssreflect +Priority: optional +Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org> +Uploaders: Stéphane Glondu <glondu@debian.org>, + Enrico Tassi <gareuselesinge@debian.org>, + Ralf Treinen <treinen@debian.org> +Build-Depends: + debhelper-compat (= 13), + coq (>= 8.7), + lua5.1 +Rules-Requires-Root: no +Standards-Version: 4.5.0 +Section: math +Homepage: https://math-comp.github.io/math-comp/ +Vcs-Browser: https://salsa.debian.org/ocaml-team/ssreflect +Vcs-Git: https://salsa.debian.org/ocaml-team/ssreflect.git + +Package: libssreflect-coq +Architecture: all +Depends: + libcoq-ocaml, + coq-${F:CoqABI}, + ${misc:Depends} +Provides: ssreflect, libmathcomp-coq +Description: Mathematical Components library for Coq + The Mathematical Components Library is an extensive and coherent + repository of formalized mathematical theories. It is based on the + Coq proof assistant, powered with the Coq/SSReflect language. + . + These formal theories cover a wide spectrum of topics, ranging from + the formal theory of general-purpose data structures like lists, + prime numbers or finite graphs, to advanced topics in algebra. + . + The formalization technique adopted in the library, called "small + scale reflection", leverages the higher-order nature of Coq's + underlying logic to provide effective automation for many small, + clerical proof steps. This is often accomplished by restating + ("reflecting") problems in a more concrete form, hence the name. For + example, arithmetic comparison is not an abstract predicate, but + rather a function computing a Boolean. + . + This package installs the full Mathematical Components library. |