Skip to content

copilot-theorem: Remove unused pragmas. Refs #613. #638

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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