From: Enrico Tassi Date: Thu, 21 Jun 2007 13:09:44 +0000 (+0000) Subject: better description X-Git-Tag: make_still_working~6244 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5e276c6a6b30e095d25847e3289fcc34f2110f55;p=helm.git better description --- diff --git a/helm/software/pkg-matita/trunk/debian/control b/helm/software/pkg-matita/trunk/debian/control index f746aacaf..4dbf9941e 100644 --- a/helm/software/pkg-matita/trunk/debian/control +++ b/helm/software/pkg-matita/trunk/debian/control @@ -2,14 +2,23 @@ Source: matita Section: math Priority: optional Maintainer: Enrico Tassi -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