diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2020-12-06
+        * Version bump (3.2).
+        * Update description, bug-reports and homepage field in cabal file
+          (#8).
+
 2019-11-22 Ivan Perez <ivan.perez@nianet.org>
         * Version bump (3.1).
         * Remove ExternFun (#6).
diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal
--- a/copilot-theorem.cabal
+++ b/copilot-theorem.cabal
@@ -5,11 +5,21 @@
 
   Some tools to prove properties on Copilot programs with k-induction model
   checking.
+  .
+  Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
+  Haskell that compiles into embedded C.  Copilot contains an interpreter,
+  multiple back-end compilers, and other verification tools.
+  .
+  A tutorial, examples, and other information are available at
+  <https://copilot-language.github.io>.
 
-version                   : 3.1
+
+version                   : 3.2
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : jonathan.laurent@ens.fr
+homepage                  : https://copilot-language.github.io
+bug-reports               : https://github.com/Copilot-Language/copilot-theorem/issues
 stability                 : Experimental
 category                  : Language, Embedded
 build-type                : Simple
@@ -56,7 +66,7 @@
                           , transformers  >= 0.5 && < 0.6
                           , xml           >= 1.3 && < 1.4
 
-                          , copilot-core  >= 3.1 && < 3.2
+                          , copilot-core  >= 3.2 && < 3.3
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove