diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,9 @@
+2021-08-19
+        * Version bump (3.5). (#247)
+        * Update travis domain in README. (#222)
+        * Remove unused type U2. (#91)
+        * Update official maintainer. (#236, #245)
+
 2021-07-07
         * Version bump (3.4). (#231)
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-[![Build Status](https://travis-ci.org/Copilot-Language/copilot.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot)
+[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://travis-ci.com/Copilot-Language/copilot)
 
 # Copilot Theorem
 
diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal
--- a/copilot-theorem.cabal
+++ b/copilot-theorem.cabal
@@ -14,10 +14,10 @@
   <https://copilot-language.github.io>.
 
 
-version                   : 3.4
+version                   : 3.5
 license                   : BSD3
 license-file              : LICENSE
-maintainer                : jonathan.laurent@ens.fr
+maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>
 homepage                  : https://copilot-language.github.io
 bug-reports               : https://github.com/Copilot-Language/copilot/issues
 stability                 : Experimental
@@ -72,7 +72,7 @@
                           , xml           >= 1.3 && < 1.4
                           , what4         >= 1.1 && < 1.2
 
-                          , copilot-core  >= 3.4 && < 3.5
+                          , copilot-core  >= 3.5 && < 3.6
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
diff --git a/src/Copilot/Theorem/Kind2/Translate.hs b/src/Copilot/Theorem/Kind2/Translate.hs
--- a/src/Copilot/Theorem/Kind2/Translate.hs
+++ b/src/Copilot/Theorem/Kind2/Translate.hs
@@ -26,11 +26,11 @@
 
 --------------------------------------------------------------------------------
 
-{- The following properties MUST hold for the given transition system :
-   * Nodes are sorted by topological order
-   * Nodes are `completed`, which means the dependency graph is transitive
-     and each node imports all the local variables of its dependencies
--}
+-- The following properties MUST hold for the given transition system :
+-- * Nodes are sorted by topological order
+-- * Nodes are `completed`, which means the dependency graph is transitive
+--   and each node imports all the local variables of its dependencies
+--
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Copilot/Theorem/TransSys/Type.hs b/src/Copilot/Theorem/TransSys/Type.hs
--- a/src/Copilot/Theorem/TransSys/Type.hs
+++ b/src/Copilot/Theorem/TransSys/Type.hs
@@ -7,7 +7,6 @@
 module Copilot.Theorem.TransSys.Type
   ( Type (..)
   , U (..)
-  , U2 (..)
   ) where
 
 import Copilot.Core.Type.Equality
@@ -35,7 +34,6 @@
 --
 -- For instance, 'U Expr' is the type of an expression of unknown type
 data U f = forall t . U (f t)
-data U2 f g = forall t . U2 (f t) (g t)
 
 --------------------------------------------------------------------------------