diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG
index f221aec44..d28cc3041 100644
--- a/copilot-theorem/CHANGELOG
+++ b/copilot-theorem/CHANGELOG
@@ -1,3 +1,6 @@
+2025-05-29
+        * Removed unused pragmas. (#613)
+
 2025-05-07
         * Version bump (4.4). (#618)
         * Translate quantifiers correctly in Kind2 backend. (#594)
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
index 66db2c346..4bb52322e 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE LambdaCase  #-}
 {-# LANGUAGE Trustworthy #-}
 
 -- | A prover backend based on Kind2.
diff --git a/copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs b/copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs
index 2ce606b31..3035f718e 100644
--- a/copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE LambdaCase     #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RankNTypes     #-}
 {-# LANGUAGE Safe           #-}
diff --git a/copilot-theorem/src/Copilot/Theorem/What4.hs b/copilot-theorem/src/Copilot/Theorem/What4.hs
index 818ac9b3a..4c9d62af8 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4.hs
@@ -1,16 +1,11 @@
 {-# LANGUAGE DataKinds                  #-}
 {-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE GADTs                      #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE KindSignatures             #-}
 {-# LANGUAGE LambdaCase                 #-}
-{-# LANGUAGE MultiWayIf                 #-}
 {-# LANGUAGE PatternSynonyms            #-}
 {-# LANGUAGE RankNTypes                 #-}
 {-# LANGUAGE ScopedTypeVariables        #-}
-{-# LANGUAGE StandaloneDeriving         #-}
-{-# LANGUAGE TemplateHaskell            #-}
-{-# LANGUAGE TupleSections              #-}
 {-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE TypeOperators              #-}