diff --git a/hylotab.cabal b/hylotab.cabal
--- a/hylotab.cabal
+++ b/hylotab.cabal
@@ -1,12 +1,11 @@
 Name:                hylotab
-Version:             1.2.0
+Version:             1.2.1
 Homepage:            http://www.glyc.dc.uba.ar/intohylo/hylotab.php
 Synopsis:            Tableau based theorem prover for hybrid logics
 Description:         HyLoTab is a proof-of-concept tableaux prover for
                      hybrid logics originally written in 2002 by Jan van Eijck.
-                     It is no longer developped, but we made it compatible
-                     with the syntax used in HyLoLib to easen comparison
-                     with other provers.
+                     It is no longer developped, but it is kept compatible
+                     with the syntax used in HyLoLib.
 License:             GPL
 License-file:        LICENSE
 Author:              Jan van Eijck, Guillaume Hoffmann
@@ -30,8 +29,8 @@
   Main-is:             Main.hs
   Other-modules:       Form Hylotab
   Build-Depends:       base >= 4, base < 5,
-                       mtl >= 1, mtl < 2,
-                       hylolib >= 1.3, hylolib < 1.4
+                       mtl >= 2, mtl < 3,
+                       hylolib == 1.4.*
   hs-source-dirs:      src
   ghc-options:          -Wall
   ghc-prof-options:    -auto-all
diff --git a/src/Form.hs b/src/Form.hs
--- a/src/Form.hs
+++ b/src/Form.hs
@@ -23,6 +23,8 @@
            | E    Form
            | Box  RelSymbol Form
            | Dia  RelSymbol Form
+           | IBox  RelSymbol Form
+           | IDia  RelSymbol Form
            | At   NomSymbol Form
            | Down NomSymbol Form
      deriving (Eq,Ord)
@@ -42,6 +44,8 @@
    show (E f)               = 'E' : show f
    show (Box name f)        = "[" ++ show name ++ "]" ++ show f
    show (Dia name f)        = "<" ++ show name ++ ">" ++ show f
+   show (IBox name f)       = "[-" ++ show name ++ "]" ++ show f
+   show (IDia name f)       = "<-" ++ show name ++ ">" ++ show f
    show (At nom f)          = show nom ++ ":" ++ show f
    show (Down i f)          = "down " ++ show i ++ "." ++ show f
 
@@ -64,6 +68,8 @@
 conv_ (f1 F.:<-->: f2) = Conj [Impl cf1 cf2, Impl cf2 cf1] where cf1 = conv_ f1 ; cf2 = conv_ f2
 conv_ (F.Diam r f)     = Dia r (conv_ f)
 conv_ (F.Box r f)      = Box r (conv_ f)
+conv_ (F.IDiam r f)    = IDia r (conv_ f)
+conv_ (F.IBox r f)     = IBox r (conv_ f)
 conv_ (F.At n f)       = At n (conv_ f)
 conv_ (F.A f)          = A (conv_ f)
 conv_ (F.E f)          = E (conv_ f)
diff --git a/src/Hylotab.hs b/src/Hylotab.hs
--- a/src/Hylotab.hs
+++ b/src/Hylotab.hs
@@ -163,6 +163,8 @@
 appF b (E f)           = E (appF b f)
 appF b (Box r f)       = Box r (appF b f)
 appF b (Dia r f)       = Dia r (appF b f)
+appF b (IBox r f)      = IBox r (appF b f)
+appF b (IDia r f)      = IDia r (appF b f)
 appF b (At n f)        = At (appNom b n) (appF b f)
 appF b (Down n f)      = Down (appNom b n) (appF b f) 
 
@@ -230,14 +232,14 @@
 isDneg _                            = False
 
 isInvRel :: Form -> Bool
-isInvRel (Box (RelSymbol _)  _)         = False
-isInvRel (Dia (RelSymbol _)  _)         = False
-isInvRel (Neg (Box (RelSymbol _)    _)) = False
-isInvRel (Neg (Dia (RelSymbol _)    _)) = False
-isInvRel (Box (InvRelSymbol _) _)       = True
-isInvRel (Dia (InvRelSymbol _) _)       = True
-isInvRel (Neg (Box (InvRelSymbol _) _)) = True
-isInvRel (Neg (Dia (InvRelSymbol _) _)) = True
+isInvRel (Box _ _)         = False
+isInvRel (Dia _ _)         = False
+isInvRel (Neg (Box _ _)) = False
+isInvRel (Neg (Dia _ _)) = False
+isInvRel (IBox _ _)       = True
+isInvRel (IDia _ _)       = True
+isInvRel (Neg (IBox _ _)) = True
+isInvRel (Neg (IDia _ _)) = True
 isInvRel f                              = error $ "error isInvRel: " ++ show f
 
 -- Function for converting a literal (a propositional atom or a negation
@@ -273,9 +275,9 @@
 getRel :: Form -> Rel
 getRel (Neg f)                           = getRel f
 getRel (Dia (RelSymbol rel) _)           = rel
-getRel (Dia (InvRelSymbol rel) _)        = rel
+getRel (IDia (RelSymbol rel) _)        = rel
 getRel (Box (RelSymbol rel) _)           = rel
-getRel (Box (InvRelSymbol rel) _)        = rel
+getRel (IBox (RelSymbol rel) _)        = rel
 getRel _                  = error "error getRel"
 
 -- The components of a (non-literal) formula are given by: