diff --git a/CHANGELOG b/CHANGELOG
new file mode 100644
--- /dev/null
+++ b/CHANGELOG
@@ -0,0 +1,3 @@
+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
@@ -6,7 +6,7 @@
   Some tools to prove properties on Copilot programs with k-induction model
   checking.
 
-version                   : 3.0
+version                   : 3.1
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : jonathan.laurent@ens.fr
@@ -14,6 +14,7 @@
 category                  : Language, Embedded
 build-type                : Simple
 extra-source-files        : README.md
+                          , CHANGELOG
 
 author                    : Jonathan Laurent
 
@@ -55,7 +56,7 @@
                           , transformers  >= 0.5 && < 0.6
                           , xml           >= 1.3 && < 1.4
 
-                          , copilot-core  >= 3.0 && < 3.1
+                          , copilot-core  >= 3.1 && < 3.2
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
diff --git a/src/Copilot/Theorem/IL/Translate.hs b/src/Copilot/Theorem/IL/Translate.hs
--- a/src/Copilot/Theorem/IL/Translate.hs
+++ b/src/Copilot/Theorem/IL/Translate.hs
@@ -36,9 +36,6 @@
 ncExternVar :: C.Name -> SeqId
 ncExternVar n = "ext_" ++ n
 
-ncExternFun :: C.Name -> SeqId
-ncExternFun n = "_" ++ n
-
 ncUnhandledOp :: String -> String
 ncUnhandledOp = id
 
@@ -135,13 +132,6 @@
 
 expr (C.ExternVar t name _) = bound s t >> return s
   where s = SVal (trType t) (ncExternVar name) _n_
-
-expr (C.ExternFun t name args _ _) = do
-  args' <- mapM trArg args
-  let s = FunApp (trType t) (ncExternFun name) args'
-  bound s t
-  return s
-  where trArg (C.UExpr {C.uExprExpr}) = expr uExprExpr
 
 expr (C.Op1 (C.Sign ta) e) = case ta of
   C.Int8   -> trSign ta e
diff --git a/src/Copilot/Theorem/TransSys/Translate.hs b/src/Copilot/Theorem/TransSys/Translate.hs
--- a/src/Copilot/Theorem/TransSys/Translate.hs
+++ b/src/Copilot/Theorem/TransSys/Translate.hs
@@ -36,7 +36,6 @@
 ncLocal s     = "l" ++ dropWhile (not . isNumber) s
 
 ncExternVarNode name = "ext-" ++ name
-ncExternFunNode name = "fun-" ++ name
 
 ncImported :: NodeId -> String -> String
 ncImported n s = n ++ ncSep ++ s
@@ -201,8 +200,6 @@
   where
     notHandled (UnhandledOp2 _opName _ta _tb _tc) =
       newUnconstrainedVar t
-
-expr t (C.ExternFun _ _ _ _ _) = newUnconstrainedVar t
 
 newUnconstrainedVar :: Type t -> Trans (Expr t)
 newUnconstrainedVar t = do