diff --git a/hylolib.cabal b/hylolib.cabal
--- a/hylolib.cabal
+++ b/hylolib.cabal
@@ -1,12 +1,12 @@
 Name:                hylolib
-Version:             1.5.2
+Version:             1.5.3
 Synopsis:            Tools for hybrid logics related programs
 License:             GPL
 License-file:        LICENSE
 Author:              Daniel Gorin
 Maintainer:          guillaumh@gmail.com
 Build-Type:          Simple
-Cabal-Version:       >= 1.22
+Cabal-Version:       >= 1.22.5
 Category:            Theorem Provers
 source-repository head
     type:     darcs
@@ -20,7 +20,7 @@
                        mtl >= 2, mtl < 3,
                        pretty >= 1, pretty < 2,
                        random >= 1, random < 2,
-                       uniplate >= 1.6, uniplate < 1.7
+                       uniplate >= 1.6.12, uniplate < 1.7
   Exposed-modules:     HyLo.Signature
                        HyLo.Signature.Simple
                        HyLo.Signature.String
@@ -42,10 +42,8 @@
                        ScopedTypeVariables
                        MultiParamTypeClasses
                        FunctionalDependencies
-                       FlexibleContexts
                        FlexibleInstances
                        UndecidableInstances
-                       PatternGuards
                        TypeFamilies
   hs-source-dirs:      src
   ghc-options:         -Wall -O2
diff --git a/src/Data/EnumMap.hs b/src/Data/EnumMap.hs
--- a/src/Data/EnumMap.hs
+++ b/src/Data/EnumMap.hs
@@ -14,11 +14,6 @@
 import Data.IntMap ( IntMap )
 import qualified Data.IntMap as IntMap
 
-import Data.Foldable ( Foldable )
-import Data.Monoid   ( Monoid )
-import Data.Typeable
-
-
 newtype EnumMap a b = EM{unEM :: IntMap b}
                       deriving ( Eq,
                                  Ord,
diff --git a/src/Data/EnumSet.hs b/src/Data/EnumSet.hs
--- a/src/Data/EnumSet.hs
+++ b/src/Data/EnumSet.hs
@@ -13,10 +13,6 @@
 import Data.IntSet ( IntSet )
 import qualified Data.IntSet as IntSet
 
-import Data.Monoid   ( Monoid )
-import Data.Typeable
-
-
 newtype EnumSet a = ES{unES :: IntSet}
                     deriving ( Eq,
                                Ord,
diff --git a/src/HyLo/Formula.hs b/src/HyLo/Formula.hs
--- a/src/HyLo/Formula.hs
+++ b/src/HyLo/Formula.hs
@@ -8,9 +8,7 @@
 
 import Text.Show.Functions ()
 
-import Control.Monad          ( liftM2, liftM4 )
-import Control.Monad.Identity ( runIdentity )
-import Control.Applicative    ( (<$>) )
+import Control.Monad          ( liftM2 )
 
 import Text.Read ( Read(..) )
 
@@ -20,13 +18,11 @@
 
 import qualified Data.List as List
 
-import Data.Generics.PlateDirect
+import Data.Generics.Uniplate.Direct
 
 import HyLo.Signature ( HasSignature(..),
                         emptySignature, merge,
                         addNomToSig, addPropToSig, addRelToSig )
-
-import HyLo.Signature.Simple ( NomSymbol, PropSymbol, RelSymbol )
 
 data Formula n p r = Top
                    | Bot
diff --git a/src/HyLo/Formula/Rewrite.hs b/src/HyLo/Formula/Rewrite.hs
--- a/src/HyLo/Formula/Rewrite.hs
+++ b/src/HyLo/Formula/Rewrite.hs
@@ -12,9 +12,7 @@
 import qualified Text.ParserCombinators.ReadPrec as RP
 import Text.ParserCombinators.ReadP    ( string )
 
-import qualified Data.Generics.UniplateStr as Uniplate
-
-import HyLo.Signature.Simple ( PropSymbol )
+import qualified Data.Generics.Uniplate.Operations as Uniplate
 
 data Rewr prop = Orig prop | Rewr Int
                deriving (Eq, Ord)
@@ -208,9 +206,10 @@
 isGlobalF :: RewrFormula n p r -> Bool
 isGlobalF  = maybe False (isGlobal . fst) . modality
 
-data Modality n p r = M_Box r | M_Dia  r
-                    | M_A     | M_E
-                    | M_D     | M_B
+data Modality n p r = M_Box r  | M_Dia  r
+                    | M_IBox r | M_IDia r
+                    | M_A      | M_E
+                    | M_D      | M_B
                     | M_At   n
                     | M_Down n
                     | M_Count CountOp (Where r) Int
@@ -219,6 +218,7 @@
 
 isABox :: Modality n p r -> Bool
 isABox M_Box {} = True
+isABox M_IBox {}= True
 isABox M_At  {} = True
 isABox M_Down{} = True
 isABox M_A      = True
@@ -233,6 +233,8 @@
 isGlobal :: Modality (BndInfo n) p r -> Bool
 isGlobal M_Box {}         = False
 isGlobal M_Dia {}         = False
+isGlobal M_IBox {}        = False
+isGlobal M_IDia {}        = False
 isGlobal M_Down{}         = False
 isGlobal (M_At (Bound _)) = False
 isGlobal M_D{}            = False
@@ -242,6 +244,8 @@
 apply :: Modality n p r -> Formula n p r -> Formula n p r
 apply (M_Box  r) = Box  r
 apply (M_Dia  r) = Diam r
+apply (M_IBox r) = IBox  r
+apply (M_IDia r) = IDiam r
 apply (M_At   i) = At   i
 apply (M_Down x) = Down x
 apply (M_Count c w i) = Count c w i
@@ -253,6 +257,8 @@
 dual :: Modality n p r -> Modality n p r
 dual (M_Box  r) = M_Dia  r
 dual (M_Dia  r) = M_Box  r
+dual (M_IBox r) = M_IDia r
+dual (M_IDia r) = M_IBox r
 dual m@M_At  {} = m
 dual m@M_Down{} = m
 dual  M_A       = M_E
@@ -262,14 +268,16 @@
 dual (M_Count c w i) = M_Count (negCount c) w i
 
 modality :: Formula n p r -> Maybe (Modality n p r, Formula n p r)
-modality (Diam r f) = Just (M_Dia  r, f)
-modality (Box  r f) = Just (M_Box  r, f)
-modality (At   i f) = Just (M_At   i, f)
-modality (Down x f) = Just (M_Down x, f)
-modality (A f)      = Just (M_A     , f)
-modality (E f)      = Just (M_E     , f)
-modality (D f)      = Just (M_D     , f)
-modality (B f)      = Just (M_B     , f)
+modality (Diam r f)  = Just (M_Dia  r, f)
+modality (Box  r f)  = Just (M_Box  r, f)
+modality (At   i f)  = Just (M_At   i, f)
+modality (Down x f)  = Just (M_Down x, f)
+modality (IDiam r f) = Just (M_IDia r, f)
+modality (IBox  r f) = Just (M_IBox r, f)
+modality (A f)       = Just (M_A     , f)
+modality (E f)       = Just (M_E     , f)
+modality (D f)       = Just (M_D     , f)
+modality (B f)       = Just (M_B     , f)
 modality (Count c w i f) = Just (M_Count c w i, f)
 modality _          = Nothing
 
@@ -282,6 +290,8 @@
           simpl (At   _ Bot)          = Just Bot
           simpl (Box  _ Top)          = Just Top
           simpl (Diam _ Bot)          = Just Bot
+          simpl (IBox _ Top)          = Just Top
+          simpl (IDiam _ Bot)         = Just Bot
           --
           simpl (Bot :&: _)           = Just Bot
           simpl (Top :&: f)           = Just f
diff --git a/src/HyLo/Model.hs b/src/HyLo/Model.hs
--- a/src/HyLo/Model.hs
+++ b/src/HyLo/Model.hs
@@ -9,12 +9,9 @@
 
 import Prelude hiding ( (!!) )
 
-import Control.Monad       ( filterM )
-import Control.Applicative ( (<$>) )
-
 import Data.Maybe ( fromMaybe )
 
-import Data.Foldable ( Foldable, toList )
+import Data.Foldable ( toList )
 
 import Data.Map ( Map )
 import qualified Data.Map as Map
@@ -30,9 +27,7 @@
                         HasSignature(..),
                         nomSymbols, propSymbols, relSymbols, merge )
 
-import HyLo.Signature.Simple ( NomSymbol, PropSymbol, RelSymbol )
-
-import HyLo.Formula ( Formula(..), Where(..), CountOp(..) )
+import HyLo.Formula ( Formula(..), Where(..) )
 import qualified HyLo.Formula as F
 
 data Model w n p r = Model{worlds :: Set w,
diff --git a/src/HyLo/Model/Herbrand.hs b/src/HyLo/Model/Herbrand.hs
--- a/src/HyLo/Model/Herbrand.hs
+++ b/src/HyLo/Model/Herbrand.hs
@@ -8,19 +8,14 @@
 import Data.Map ( Map )
 import qualified Data.Map as Map
 
-import Data.Foldable ( Foldable, foldMap, toList )
-
-import Text.Read ( Read(..), get, lift )
-import Text.ParserCombinators.ReadP ( skipSpaces )
+import Data.Foldable ( toList )
 
 import HyLo.Formula ( Formula(At, Nom, Prop, Diam) )
 
-import HyLo.Model ( Model, ModelsRel(..), model, equiv )
-import qualified HyLo.Model as M
+import HyLo.Model ( Model, ModelsRel(..), model )
 
 import HyLo.Signature ( HasSignature(..), Signature, merge,
                         nomSymbols, delNomFromSig )
-import HyLo.Signature.Simple ( NomSymbol, PropSymbol, RelSymbol )
 
 data HerbrandModel n p r where
     H :: (Ord n, Ord p, Ord r)
diff --git a/src/HyLo/Signature.hs b/src/HyLo/Signature.hs
--- a/src/HyLo/Signature.hs
+++ b/src/HyLo/Signature.hs
@@ -11,12 +11,8 @@
 
 where
 
-import Data.Monoid ( Monoid(..) )
-
 import Data.Set ( Set )
 import qualified Data.Set as Set
-
-import Control.Monad   ( liftM3 )
 
 data Signature n p r = Sig{nomSymbols  :: Set n,
                            propSymbols :: Set p,