Section: math
Priority: optional
Maintainer: Enrico Tassi <gareuselesinge@debian.org>
-Build-Depends: ocaml, 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-ulex, libexpat-ocaml-dev, debhelper, cdbs, libmysql-ocaml-dev
+Build-Depends: ocaml, ocaml-findlib, libgdome2-ocaml-dev, liblablgtk2-ocaml-dev, liblablgtkmathview-ocaml-dev, liblablgtksourceview-ocaml-dev, libsqlite3-ocaml-dev (>= 0.21.0), libocamlnet-ocaml-dev, libzip-ocaml-dev, libhttp-ocaml-dev, ocaml-ulex, libexpat-ocaml-dev, debhelper, cdbs, libmysql-ocaml-dev
Standards-Version: 3.7.2
Package: matita
Architecture: any
Depends: ${shlibs:Depends}
-Description: matita interactive theorem prover
- matita interactive theorem prover.
+Recommends: matita-standard-library
+Description: Matita interactive theorem prover
+ Matita is an interactive theorem prover based on the Calculus of (Co)Inductive
+ Constructions.
+
+ Matita adopts XML-encoded proof objects are produced for storage and exchange.
+ This makes it compatible, at some extent, with Coq.
+
+ The graphical interface has been inspired by CtCoq and Proof General. It
+ supports high quality bidimensional rendering of proofs and formulae
+ transformed on-the-fly to MathML markup
Package: matita-standard-library
Architecture: all