Skip to content
3 changes: 3 additions & 0 deletions copilot-theorem/CHANGELOG
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
1 change: 0 additions & 1 deletion copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Trustworthy #-}

-- | A prover backend based on Kind2.
Expand Down
1 change: 0 additions & 1 deletion copilot-theorem/src/Copilot/Theorem/Prover/SMTIO.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
Expand Down
25 changes: 10 additions & 15 deletions copilot-theorem/src/Copilot/Theorem/What4.hs
Original file line number Diff line number Diff line change
@@ -1,18 +1,13 @@
{-# 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 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- |
-- Module : Copilot.Theorem.What4
Expand Down