4 Maintainer: Enrico Tassi <gareuselesinge@debian.org>
5 Uploaders: Stefano Zacchiroli <zack@debian.org>
6 Homepage: http://matita.cs.unibo.it
7 Build-Depends: ocaml (>= 3.10.0), ocaml-findlib, libgdome2-ocaml-dev, liblablgtk2-ocaml-dev, liblablgtkmathview-ocaml-dev, liblablgtksourceview-ocaml-dev, libsqlite3-ocaml-dev, libocamlnet-ocaml-dev, libzip-ocaml-dev, libhttp-ocaml-dev, ocaml-ulex08, libexpat-ocaml-dev, debhelper, cdbs, libmysql-ocaml-dev, camlp5, dpatch, help2man
8 Standards-Version: 3.7.2
9 XS-Vcs-Svn: svn://mowgli.cs.unibo.it/trunk/helm/software/pkg-matita/trunk/
10 XS-Vcs-Browser: http://helm.cs.unibo.it/websvn/listing.php?path=/trunk/helm/software/pkg-matita/trunk/
14 Depends: ${shlibs:Depends}
15 Recommends: matita-standard-library, graphviz
16 Description: interactive theorem prover
17 Matita is a graphical interactive theorem prover based on the Calculus of
18 (Co)Inductive Constructions.
20 Matita adopts XML-encoded proof objects are produced for storage and exchange.
21 This makes it compatible, at some extent, with Coq.
23 The graphical interface has been inspired by CtCoq and Proof General. It
24 supports high quality bidimensional rendering of proofs and formulae
25 transformed on-the-fly to MathML markup
27 Package: matita-standard-library
29 Depends: matita (= ${binary:Version})
30 Description: standard library for the Matita interactive theorem prover
31 Matita is a graphical interactive theorem prover based on the Calculus of
32 (Co)Inductive Constructions.
34 This package contains the standard library of theorems of the
35 matita interactive theorem prover.