diff options
Diffstat (limited to 'debian/control')
-rw-r--r-- | debian/control | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/debian/control b/debian/control new file mode 100644 index 0000000..f4bf585 --- /dev/null +++ b/debian/control @@ -0,0 +1,59 @@ +Source: aac-tactics +Section: math +Priority: optional +Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org> +Uploaders: Stéphane Glondu <glondu@debian.org> +Build-Depends: + debhelper (>= 9), + dh-ocaml (>= 0.9~), + ocaml-nox (>= 3.11.1-3~), + coq (>= 8.4dfsg-2~), + libcoq-ocaml-dev +Standards-Version: 3.9.8 +Homepage: https://github.com/coq-contribs/aac-tactics +Vcs-Browser: https://anonscm.debian.org/cgit/pkg-ocaml-maint/packages/aac-tactics.git +Vcs-Git: https://anonscm.debian.org/git/pkg-ocaml-maint/packages/aac-tactics.git + +Package: libaac-tactics-ocaml +Section: ocaml +Architecture: any +Depends: + ${ocaml:Depends}, + ${shlibs:Depends}, + ${misc:Depends} +Recommends: libaac-tactics-coq +Enhances: coq +Provides: ${ocaml:Provides} +Description: Coq tactics for reasoning modulo AC (plugin) + This Coq plugin provides tactics for rewriting universally quantified + equations, modulo associative (and possibly commutative) operators. + . + This package provides the plugin itself. + +Package: libaac-tactics-ocaml-dev +Section: ocaml +Architecture: any +Depends: + ${ocaml:Depends}, + ${shlibs:Depends}, + ${misc:Depends} +Provides: ${ocaml:Provides} +Description: Coq tactics for reasoning modulo AC (devt files) + This Coq plugin provides tactics for rewriting universally quantified + equations, modulo associative (and possibly commutative) operators. + . + This package provides the static native-code library, needed to build + custom toplevels, and the compiled interfaces. + +Package: libaac-tactics-coq +Architecture: all +Depends: + libaac-tactics-ocaml (>= ${source:Version}), + coq-${F:CoqABI}, + ${misc:Depends} +Provides: aac-tactics +Description: Coq tactics for reasoning modulo AC (theories) + This Coq plugin provides tactics for rewriting universally quantified + equations, modulo associative (and possibly commutative) operators. + . + This package provides the Coq support library. |