diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,7 @@
+2022-03-07
+        * Version bump (3.8). (#298)
+        * Mark package as uncurated to avoid modification. (#288)
+
 2022-01-07
         * Version bump (3.7). (#287)
         * Relax version contraints on what4. (#277)
diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal
--- a/copilot-theorem.cabal
+++ b/copilot-theorem.cabal
@@ -14,7 +14,7 @@
   <https://copilot-language.github.io>.
 
 
-version                   : 3.7
+version                   : 3.8
 license                   : BSD3
 license-file              : LICENSE
 maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>
@@ -28,6 +28,8 @@
 
 author                    : Jonathan Laurent
 
+x-curation: uncurated
+
 library
   default-language        : Haskell2010
   hs-source-dirs          : src
@@ -72,7 +74,7 @@
                           , xml           >= 1.3 && < 1.4
                           , what4         >= 1.1 && < 1.3
 
-                          , copilot-core  >= 3.7 && < 3.8
+                          , copilot-core  >= 3.8 && < 3.9
 
   exposed-modules         : Copilot.Theorem
                           , Copilot.Theorem.Prove
diff --git a/src/Copilot/Theorem/TransSys/Cast.hs b/src/Copilot/Theorem/TransSys/Cast.hs
--- a/src/Copilot/Theorem/TransSys/Cast.hs
+++ b/src/Copilot/Theorem/TransSys/Cast.hs
@@ -17,9 +17,8 @@
 --------------------------------------------------------------------------------
 
 import Copilot.Core as C
-import Copilot.Core.Type.Equality
-import Copilot.Core.Type.Dynamic
 
+import Data.Dynamic (Dynamic(..), fromDynamic, toDyn)
 import GHC.Float
 
 import qualified Copilot.Theorem.TransSys.Type as K
@@ -27,7 +26,7 @@
 --------------------------------------------------------------------------------
 
 -- | Synonym for a dynamic type in Copilot core.
-type Dyn = Dynamic Type
+type Dyn = Dynamic
 
 -- | Translation of a Copilot type into Copilot theorem's internal
 -- representation.
@@ -67,26 +66,26 @@
   _cast :: Dyn -> Maybe b
 
 instance Casted Integer where
-  _cast (Dynamic v tv)
-    | Just Refl <- tv =~= Int8    = Just $ toInteger v
-    | Just Refl <- tv =~= Int16   = Just $ toInteger v
-    | Just Refl <- tv =~= Int32   = Just $ toInteger v
-    | Just Refl <- tv =~= Int64   = Just $ toInteger v
-    | Just Refl <- tv =~= Word16  = Just $ toInteger v
-    | Just Refl <- tv =~= Word8   = Just $ toInteger v
-    | Just Refl <- tv =~= Word32  = Just $ toInteger v
-    | Just Refl <- tv =~= Word64  = Just $ toInteger v
-    | otherwise                   = Nothing
+  _cast d
+    | Just (v :: Int8)   <- fromDynamic d = Just $ toInteger v
+    | Just (v :: Int16)  <- fromDynamic d = Just $ toInteger v
+    | Just (v :: Int32)  <- fromDynamic d = Just $ toInteger v
+    | Just (v :: Int64)  <- fromDynamic d = Just $ toInteger v
+    | Just (v :: Word8)  <- fromDynamic d = Just $ toInteger v
+    | Just (v :: Word16) <- fromDynamic d = Just $ toInteger v
+    | Just (v :: Word32) <- fromDynamic d = Just $ toInteger v
+    | Just (v :: Word64) <- fromDynamic d = Just $ toInteger v
+    | otherwise                           = Nothing
 
 instance Casted Bool where
-  _cast (Dynamic v tv)
-    | Just Refl <- tv =~= Bool  = Just v
-    | otherwise                 = Nothing
+  _cast d
+    | Just (v :: Bool) <- fromDynamic d = Just v
+    | otherwise                         = Nothing
 
 instance Casted Double where
-  _cast (Dynamic v tv)
-    | Just Refl <- tv =~= Float  = Just $ float2Double v
-    | Just Refl <- tv =~= Double = Just v
-    | otherwise = Nothing
+  _cast d
+    | Just (v :: Float)  <- fromDynamic d = Just $ float2Double v
+    | Just (v :: Double) <- fromDynamic d = Just v
+    | otherwise                           = Nothing
 
 --------------------------------------------------------------------------------
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
@@ -161,7 +161,7 @@
 
     let nodeId = ncNode streamId
         outvar i = Var (ncMain `ncTimeAnnot` i)
-        buf = map (cast t . toDyn streamExprType) streamBuffer
+        buf = map (cast t . toDyn) streamBuffer
 
     (e, nodeAuxVars, nodeImportedVars, nodeDependencies) <-
       runExprTrans t nodeId streamExpr
@@ -184,7 +184,7 @@
 
 expr :: Type t -> C.Expr t' -> Trans (Expr t)
 
-expr t (C.Const t' v) = return $ Const t (cast t $ toDyn t' v)
+expr t (C.Const _ v) = return $ Const t (cast t $ toDyn v)
 
 expr t (C.Drop _ (fromIntegral -> k :: Int) id) = do
   let node = ncNode id