The following commit has been merged in the experimental/master branch:
commit 9d5c2db60be06d2ba57204c8a2cff417d69a4b74
Author: Ralf Treinen <>
Date:   Tue Apr 9 16:43:34 2013 +0200

    rewrite long package description

diff --git a/debian/changelog b/debian/changelog
index fbf5471..ff566d3 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -28,8 +28,9 @@ alt-ergo (0.95.1-1) UNRELEASED; urgency=low
     - debian/control: drop quilt from build-dependencies
   * Drop build-dependencies on autotools-dev, autoconf which are not needed.
     Touch configure in debian/rules to assure it is newer than
- -- Ralf Treinen <>  Sat, 06 Apr 2013 11:43:07 +0200
+  * Rewrite long package description.
+ -- Ralf Treinen <>  Tue, 09 Apr 2013 16:43:00 +0200
 alt-ergo (0.94-2) unstable; urgency=high
diff --git a/debian/control b/debian/control
index fe20713..f695f0f 100644
--- a/debian/control
+++ b/debian/control
@@ -22,11 +22,12 @@ Architecture: any
 Depends: ${shlibs:Depends}, ${misc:Depends}, ${ocaml:Depends}
 Suggests: why
 Description: Automatic theorem prover dedicated to program verification
- Alt-Ergo is an automatic theorem prover dedicated to program verification. 
- Alt-Ergo is based on CC(X) a congruence closure algorithm parameterized by an 
- equational theory X. Currently, CC(X) can be instantiated by the empty 
- equational theory and by the linear arithmetics. Alt-Ergo contains also a 
- made SAT-solver and an instantiation mechanism.
- .
- Alt-Ergo is both safe and modular: each box is described by a small set of 
- inference rules and is implemented as an OCaml functor.
+ Alt-Ergo is an automatic theorem prover geared towards application in
+ program verification. It is based on CC(X), a congruence closure
+ algorithm parameterized by an equational theory X. Alt-Ergo has
+ built-in provers for propositional logic, linear arithmetic,
+ uninterpreted function symbols, associative-commutative function
+ symbols, polymorphic arrays, user-defined polymorphic record types
+ and polymorphic enumeration types. It has restricted support for
+ reasoning over arbitrary user-defined algebraic types, first-order
+ quantifiers, and non-linear arithmetic.

alt-ergo packaging

Pkg-ocaml-maint-commits mailing list

Reply via email to