diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2023-05-07
+        * Version bump (3.15). (#438)
+        * Remove Copilot.Core.Type.Equality. (#427)
+        * Remove Copilot.Core.PrettyPrint. (#426)
+
 2023-03-07
         * Version bump (3.14). (#422)
         * Remove Copilot.Core.PrettyDot. (#409)
diff --git a/copilot-core.cabal b/copilot-core.cabal
--- a/copilot-core.cabal
+++ b/copilot-core.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-core
-version:             3.14
+version:             3.15
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
@@ -42,8 +42,7 @@
     -fno-warn-orphans
 
   build-depends:
-    base       >= 4.9 && < 5,
-    pretty     >= 1.0 && < 1.2
+    base >= 4.9 && < 5
 
   exposed-modules:
 
@@ -53,14 +52,7 @@
     Copilot.Core.Spec
     Copilot.Core.Type
     Copilot.Core.Type.Array
-    Copilot.Core.Type.Equality
-    Copilot.Core.PrettyPrint
 
-  other-modules:
-
-    Copilot.Core.Error
-    Copilot.Core.Type.Show
-
 test-suite unit-tests
   type:
     exitcode-stdio-1.0
@@ -77,7 +69,6 @@
       base
     , HUnit
     , QuickCheck
-    , pretty
     , test-framework
     , test-framework-hunit
     , test-framework-quickcheck2
diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs
--- a/src/Copilot/Core.hs
+++ b/src/Copilot/Core.hs
@@ -17,8 +17,7 @@
 --
 -- For examples of how to traverse a Copilot specification see
 -- the source code of the interpreter (@copilot-interpreter@)
--- and the pretty-printer
--- ("Copilot.Core.PrettyPrint").
+-- and the pretty-printer (@copilot-prettyprinter@).
 module Copilot.Core
     ( module Copilot.Core.Expr
     , module Copilot.Core.Operators
diff --git a/src/Copilot/Core/Error.hs b/src/Copilot/Core/Error.hs
deleted file mode 100644
--- a/src/Copilot/Core/Error.hs
+++ /dev/null
@@ -1,20 +0,0 @@
-{-# LANGUAGE Safe #-}
-
--- |
--- Description: Custom functions to report error messages to users.
--- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
-module Copilot.Core.Error
-    ( impossible
-    )
-  where
-
--- | Report an error due to a bug in Copilot.
-impossible :: String -- ^ Name of the function in which the error was detected.
-           -> String -- ^ Name of the package in which the function is located.
-           -> a
-impossible function package =
-  error $ "\"Impossible\" error in function "
-    ++ function ++ ", in package " ++ package
-    ++ ". Please file an issue at "
-    ++ "https://github.com/Copilot-Language/copilot/issues"
-    ++ "or email the maintainers at <ivan.perezdominguez@nasa.gov>"
diff --git a/src/Copilot/Core/PrettyPrint.hs b/src/Copilot/Core/PrettyPrint.hs
deleted file mode 100644
--- a/src/Copilot/Core/PrettyPrint.hs
+++ /dev/null
@@ -1,195 +0,0 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
--- | A pretty printer for Copilot specifications.
-
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE Safe  #-}
-
-module Copilot.Core.PrettyPrint
-  {-# DEPRECATED "This module is deprecated in Copilot 3.12. Use copilot-prettyprinter instead." #-}
-  ( prettyPrint
-  , ppExpr
-  ) where
-
-import Copilot.Core
-import Copilot.Core.Error (impossible)
-import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)
-import Prelude hiding (id, (<>))
-import Text.PrettyPrint.HughesPJ
-import Data.List (intersperse)
-
--- | Create a unique stream name by prefixing the given ID by a lowercase
--- letter @"s"@.
-strmName :: Int -> Doc
-strmName id = text "s" <> int id
-
--- | Pretty-print a Copilot expression.
---
--- The type is ignored, and only the expression is pretty-printed.
-ppExpr :: Expr a -> Doc
-ppExpr e0 = case e0 of
-  Const t x                  -> text (showWithType Haskell t x)
-  Drop _ 0 id                -> strmName id
-  Drop _ i id                -> text "drop" <+> text (show i) <+> strmName id
-  ExternVar _ name _         -> text "Ext_" <> (text name)
-  Local _ _ name e1 e2       -> text "local" <+> doubleQuotes (text name) <+> equals
-                                          <+> ppExpr e1 $$ text "in" <+> ppExpr e2
-  Var _ name                 -> text "var" <+> doubleQuotes (text name)
-  Op1 op e                   -> ppOp1 op (ppExpr e)
-  Op2 op e1 e2               -> ppOp2 op (ppExpr e1) (ppExpr e2)
-  Op3 op e1 e2 e3            -> ppOp3 op (ppExpr e1) (ppExpr e2) (ppExpr e3)
-  Label _ s e                -> text "label "<> doubleQuotes (text s) <+> (ppExpr e)
-
--- | Pretty-print an untyped expression.
---
--- The type is ignored, and only the expression is pretty-printed.
-ppUExpr :: UExpr -> Doc
-ppUExpr UExpr { uExprExpr = e0 } = ppExpr e0
-
--- | Pretty-print a unary operation.
-ppOp1 :: Op1 a b -> Doc -> Doc
-ppOp1 op = case op of
-  Not                     -> ppPrefix "not"
-  Abs _                   -> ppPrefix "abs"
-  Sign _                  -> ppPrefix "signum"
-  Recip _                 -> ppPrefix "recip"
-  Exp _                   -> ppPrefix "exp"
-  Sqrt _                  -> ppPrefix "sqrt"
-  Log _                   -> ppPrefix "log"
-  Sin _                   -> ppPrefix "sin"
-  Tan _                   -> ppPrefix "tan"
-  Cos _                   -> ppPrefix "cos"
-  Asin _                  -> ppPrefix "asin"
-  Atan _                  -> ppPrefix "atan"
-  Acos _                  -> ppPrefix "acos"
-  Sinh _                  -> ppPrefix "sinh"
-  Tanh _                  -> ppPrefix "tanh"
-  Cosh _                  -> ppPrefix "cosh"
-  Asinh _                 -> ppPrefix "asinh"
-  Atanh _                 -> ppPrefix "atanh"
-  Acosh _                 -> ppPrefix "acosh"
-  Ceiling _               -> ppPrefix "ceiling"
-  Floor _                 -> ppPrefix "floor"
-  BwNot _                 -> ppPrefix "~"
-  Cast _ _                -> ppPrefix "(cast)"
-  GetField (Struct _) _ f -> \e -> ppInfix "#" e (text $ accessorname f)
-  GetField _ _ _          -> impossible "ppOp1" "Copilot.Core.PrettyPrint"
-
--- | Pretty-print a binary operation.
-ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc
-ppOp2 op = case op of
-  And          -> ppInfix "&&"
-  Or           -> ppInfix "||"
-  Add      _   -> ppInfix "+"
-  Sub      _   -> ppInfix "-"
-  Mul      _   -> ppInfix "*"
-  Div      _   -> ppInfix "div"
-  Mod      _   -> ppInfix "mod"
-  Fdiv     _   -> ppInfix "/"
-  Pow      _   -> ppInfix "**"
-  Logb     _   -> ppInfix "logBase"
-  Atan2    _   -> ppInfix "atan2"
-  Eq       _   -> ppInfix "=="
-  Ne       _   -> ppInfix "/="
-  Le       _   -> ppInfix "<="
-  Ge       _   -> ppInfix ">="
-  Lt       _   -> ppInfix "<"
-  Gt       _   -> ppInfix ">"
-  BwAnd    _   -> ppInfix "&"
-  BwOr     _   -> ppInfix "|"
-  BwXor    _   -> ppInfix "^"
-  BwShiftL _ _ -> ppInfix "<<"
-  BwShiftR _ _ -> ppInfix ">>"
-  Index    _   -> ppInfix ".!!"
-
--- | Pretty-print a ternary operation.
-ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc
-ppOp3 op = case op of
-  Mux _    -> \ doc1 doc2 doc3 ->
-    text "(if"   <+> doc1 <+>
-    text "then" <+> doc2 <+>
-    text "else" <+> doc3 <> text ")"
-
--- | Parenthesize two 'Doc's, separated by an infix 'String'.
-ppInfix :: String -> Doc -> Doc -> Doc
-ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2
-
--- | Prefix a 'Doc' by a 'String'.
-ppPrefix :: String -> Doc -> Doc
-ppPrefix cs = (text cs <+>)
-
--- | Pretty-print a Copilot stream as a case of a top-level function for
--- streams of that type, by pattern matching on the stream name.
-ppStream :: Stream -> Doc
-ppStream
-  Stream
-    { streamId       = id
-    , streamBuffer   = buffer
-    , streamExpr     = e
-    , streamExprType = t
-    }
-      = (parens . text . showType) t
-          <+> strmName id
-    <+> text "="
-    <+> text ("["
-              ++ ( concat $ intersperse ","
-                              $ map (showWithType Haskell t) buffer )
-              ++ "]")
-    <+> text "++"
-    <+> ppExpr e
-
--- | Pretty-print a Copilot trigger as a case of a top-level @trigger@
--- function, by pattern matching on the trigger name.
-ppTrigger :: Trigger -> Doc
-ppTrigger
-  Trigger
-    { triggerName  = name
-    , triggerGuard = e
-    , triggerArgs  = args }
-  =   text "trigger" <+> text "\"" <> text name <> text "\""
-  <+> text "="
-  <+> ppExpr e
-  <+> lbrack
-  $$  (nest 2 $ vcat (punctuate comma $
-                          map (\a -> text "arg" <+> ppUExpr a) args))
-  $$  nest 2 rbrack
-
--- | Pretty-print a Copilot observer as a case of a top-level @observer@
--- function, by pattern matching on the observer name.
-ppObserver :: Observer -> Doc
-ppObserver
-  Observer
-    { observerName     = name
-    , observerExpr     = e }
-  =   text "observer \"" <> text name <> text "\""
-  <+> text "="
-  <+> ppExpr e
-
--- | Pretty-print a Copilot property as a case of a top-level @property@
--- function, by pattern matching on the property name.
-ppProperty :: Property -> Doc
-ppProperty
-  Property
-    { propertyName     = name
-    , propertyExpr     = e }
-  =   text "property \"" <> text name <> text "\""
-  <+> text "="
-  <+> ppExpr e
-
--- | Pretty-print a Copilot specification, in the following order:
---
--- - Streams definitions
--- - Trigger definitions
--- - Observer definitions
--- - Property definitions
-ppSpec :: Spec -> Doc
-ppSpec spec = cs $$ ds $$ es $$ fs
-  where
-    cs = foldr (($$) . ppStream)   empty (specStreams   spec)
-    ds = foldr (($$) . ppTrigger)  empty (specTriggers  spec)
-    es = foldr (($$) . ppObserver) empty (specObservers spec)
-    fs = foldr (($$) . ppProperty) empty (specProperties spec)
-
--- | Pretty-print a Copilot specification.
-prettyPrint :: Spec -> String
-prettyPrint = render . ppSpec
diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs
--- a/src/Copilot/Core/Type.hs
+++ b/src/Copilot/Core/Type.hs
@@ -8,11 +8,6 @@
 {-# LANGUAGE ScopedTypeVariables       #-}
 {-# LANGUAGE TypeOperators             #-}
 {-# LANGUAGE UndecidableInstances      #-}
-
--- The following flag is disabled in this module so that the import of
--- Copilot.Core.Type.Equality does not give rise to warnings.
-{-# OPTIONS_GHC -fno-warn-deprecations #-}
-
 -- |
 -- Description: Typing for Core.
 -- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
@@ -53,8 +48,7 @@
                            symbolVal)
 
 -- Internal imports
-import Copilot.Core.Type.Array    (Array)
-import Copilot.Core.Type.Equality as CE
+import Copilot.Core.Type.Array (Array)
 
 -- | The value of that is a product or struct, defined as a constructor with
 -- several fields.
@@ -122,20 +116,6 @@
 tysize :: forall n t . KnownNat n => Type (Array n t) -> Int
 tysize ty@(Array ty'@(Array _)) = tylength ty * tysize ty'
 tysize ty@(Array _            ) = tylength ty
-
-instance EqualType Type where
-  (=~=) Bool   Bool   = Just CE.Refl
-  (=~=) Int8   Int8   = Just CE.Refl
-  (=~=) Int16  Int16  = Just CE.Refl
-  (=~=) Int32  Int32  = Just CE.Refl
-  (=~=) Int64  Int64  = Just CE.Refl
-  (=~=) Word8  Word8  = Just CE.Refl
-  (=~=) Word16 Word16 = Just CE.Refl
-  (=~=) Word32 Word32 = Just CE.Refl
-  (=~=) Word64 Word64 = Just CE.Refl
-  (=~=) Float  Float  = Just CE.Refl
-  (=~=) Double Double = Just CE.Refl
-  (=~=) _ _ = Nothing
 
 instance TestEquality Type where
   testEquality Bool   Bool   = Just DE.Refl
diff --git a/src/Copilot/Core/Type/Equality.hs b/src/Copilot/Core/Type/Equality.hs
deleted file mode 100644
--- a/src/Copilot/Core/Type/Equality.hs
+++ /dev/null
@@ -1,46 +0,0 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
-{-# LANGUAGE GADTs          #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE Safe           #-}
-
--- | Propositional equality and type equality.
-module Copilot.Core.Type.Equality
-  {-# DEPRECATED "This module is deprecated in Copilot 3.12. Use base:Data.Type.Equality instead." #-}
-  ( Equal (..)
-  , EqualType (..)
-  , coerce
-  , refl
-  , trans
-  , symm
-  , cong
-  ) where
-
--- | Propositional equality.
-data Equal :: * -> * -> * where
-  Refl :: Equal a a
-
--- | Type equality. If the value of @x =~= y@ is @Just Refl@, then the two
--- types @x@ and @y@ are equal.
-class EqualType t where
-  (=~=) :: t a -> t b -> Maybe (Equal a b)
-
--- | Safe coercion, which requires proof of equality.
-coerce :: Equal a b -> a -> b
-coerce Refl x = x
-
--- | Proof of propositional equality.
-refl :: Equal a a
-refl = Refl
-
--- | Symmetry.
-symm :: Equal a b -> Equal b a
-symm Refl = Refl
-
--- | Transitivity.
-trans :: Equal a b -> Equal b c -> Equal a c
-trans Refl Refl = Refl
-
--- | Congruence.
-cong :: Equal a b -> Equal (f a) (f b)
-cong Refl = Refl
diff --git a/src/Copilot/Core/Type/Show.hs b/src/Copilot/Core/Type/Show.hs
deleted file mode 100644
--- a/src/Copilot/Core/Type/Show.hs
+++ /dev/null
@@ -1,77 +0,0 @@
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE GADTs                     #-}
-{-# LANGUAGE Safe                      #-}
-
--- |
--- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
---
--- Show Copilot Core types and typed values.
-module Copilot.Core.Type.Show
-    ( showWithType
-    , ShowType (..)
-    , showType
-    )
-  where
-
--- Internal imports
-import Copilot.Core.Type (Type (..))
-
--- | Target language for showing a typed value. Used to adapt the
--- representation of booleans.
-data ShowType = C | Haskell
-
--- | Show a value. The representation depends on the type and the target
--- language. Booleans are represented differently depending on the backend.
-showWithType :: ShowType -> Type a -> a -> String
-showWithType showT t x =
-    case showT of
-      C       -> case t of
-                   Bool -> if x then "1" else "0"
-                   _    -> sw
-      Haskell -> case t of
-                   Bool -> if x then "true" else "false"
-                   _    -> sw
-  where
-    sw = case showWit t of
-           ShowWit -> show x
-
--- | Show Copilot Core type.
-showType :: Type a -> String
-showType t =
-  case t of
-    Bool     -> "Bool"
-    Int8     -> "Int8"
-    Int16    -> "Int16"
-    Int32    -> "Int32"
-    Int64    -> "Int64"
-    Word8    -> "Word8"
-    Word16   -> "Word16"
-    Word32   -> "Word32"
-    Word64   -> "Word64"
-    Float    -> "Float"
-    Double   -> "Double"
-    Array t  -> "Array " ++ showType t
-    Struct t -> "Struct"
-
--- * Auxiliary show instance
-
--- | Witness datatype for showing a value, used by 'showWithType'.
-data ShowWit a = Show a => ShowWit
-
--- | Turn a type into a show witness.
-showWit :: Type a -> ShowWit a
-showWit t =
-  case t of
-    Bool     -> ShowWit
-    Int8     -> ShowWit
-    Int16    -> ShowWit
-    Int32    -> ShowWit
-    Int64    -> ShowWit
-    Word8    -> ShowWit
-    Word16   -> ShowWit
-    Word32   -> ShowWit
-    Word64   -> ShowWit
-    Float    -> ShowWit
-    Double   -> ShowWit
-    Array t  -> ShowWit
-    Struct t -> ShowWit