diff --git a/hgen.cabal b/hgen.cabal
--- a/hgen.cabal
+++ b/hgen.cabal
@@ -1,5 +1,5 @@
 Name:                hgen
-Version:             1.2.0
+Version:             1.4.0
 Synopsis:            Random generation of modal and hybrid logic formulas
 Description:         Random generation of modal and hybrid logic formulas
 Category:            Theorem Provers
@@ -9,7 +9,7 @@
 Maintainer:          areces@loria.fr
 Homepage:            http://www.glyc.dc.uba.ar/intohylo/hgen.php
 Build-type:          Simple
-Cabal-version:       >= 1.2
+Cabal-version:       >= 1.6
 
 Flag static
   Description: Build a static binary
@@ -22,10 +22,10 @@
   ghc-options:         -Wall
   Build-Depends:       base >= 4, base < 5,
                        random >= 1, random < 2,
-                       mtl >= 1, mtl < 2,
+                       mtl >= 2, mtl < 3,
                        filepath >= 1, filepath < 2,
                        directory >= 1, directory < 2,
-                       hylolib >= 1.3, hylolib < 1.4
+                       hylolib == 1.4.*
 
   if flag(static)
     ghc-options: -static -optl-static -optl-pthread
diff --git a/src/Params.hs b/src/Params.hs
--- a/src/Params.hs
+++ b/src/Params.hs
@@ -76,18 +76,10 @@
           ["help"]
           (NoArg $ \p -> return p{showHelp = True})
           "display this help and exit",
-   Option ['o']
-          ["stdout"]
-          (NoArg $ \p -> return p{stdout = True})
-           "display on stdout instead of writing output into files",
    Option ['H']
           ["hide-summary"]
           (NoArg $ \p -> return p{hidesummary = True})
            "hide summary of the options used",
-   Option []
-          ["simple"]
-           (NoArg $ \p -> return p{simpleFormat = True})
-           "output formulas in simple format",
    Option ['#']
           ["num-inst"]
           (ReqArg ((not . null) ?-> \s p -> return p{numinst = read s}) "INT")
diff --git a/src/hgen.hs b/src/hgen.hs
--- a/src/hgen.hs
+++ b/src/hgen.hs
@@ -57,7 +57,7 @@
                     dzero (umdepth p)  * puniv p,
                     dzero (dumdepth p) * pduniv p,
                     dzero (invdepth p) * pinv p]
-              else [pmod p, pat p, pdown p, pduniv p, pinv p]
+              else [pmod p, pat p, pdown p, puniv p, pduniv p, pinv p]
 
 -- probsProp : Given the set of parameters (which varies as the
 -- formula grows) and a list of atoms, it returns the probability of an
@@ -96,11 +96,7 @@
 runWithParams params =
    do unless (hidesummary params) $ putStr $ "Setting the following parameters:\n" ++ show params
       frmList     <- evalState (generateFormulaList (numinst params) params) `fmap` newStdGen
-      let output  = if stdout params then putStrLn . unwords else writeList (getName params) (numinst params)
-      output $
-        if simpleFormat params
-         then frmList
-         else map ("signature { automatic }\n\ntheory" ++) frmList
+      writeList (getName params) (numinst params) frmList
 
 getName :: Params -> String
 getName params
@@ -365,7 +361,7 @@
     do shapes <- genShape (numclauses p) (gdepth p) p
        gd <- genDisjunctList shapes p
        newf <- mapM (sanitize2 p) gd
-       return $ write p $ map toHyLoFormula newf
+       return $ write $ map toHyLoFormula newf
 
 hmpro :: Formula -> Int
 hmpro (Fprop _)   = 1
@@ -376,6 +372,7 @@
 hmpro (Fdubox f)  = hmpro f
 hmpro (For fl)    = sum (map hmpro fl)
 hmpro (Fbox _ f)  = hmpro f
+hmpro (Fibox _ f) = hmpro f
 hmpro (Fat _ f)   = hmpro f
 hmpro (Fatv _ f)  = hmpro f
 hmpro (Fdown _ f) = hmpro f
@@ -390,6 +387,7 @@
 hmnom (Fdubox f)  = hmnom f
 hmnom (For fl)    = sum (map hmnom fl)
 hmnom (Fbox _ f)  = hmnom f
+hmnom (Fibox _ f) = hmnom f
 hmnom (Fat _ f)   = hmnom f
 hmnom (Fatv _ f)  = hmnom f
 hmnom (Fdown _ f) = hmnom f
@@ -404,6 +402,7 @@
 hmat (Fdubox f)   = hmat f
 hmat (For fl)     = sum (map hmat fl)
 hmat (Fbox _ f)   = hmat f
+hmat (Fibox _ f)  = hmat f
 hmat (Fat _ f)    = 1 + hmat f
 hmat (Fatv _ f)   = hmat f
 hmat (Fdown _ f)  = hmat f
@@ -586,9 +585,8 @@
  show (RelSymbol i)    =  'R'  : show i
  show (InvRelSymbol i) = "-R" ++ show i
 
-write :: Params -> [HyLoFormula] -> String
-write params input = unlines $ beginMark:addSemicolon (map show input) ++ [endMark]
+write :: [HyLoFormula] -> String
+write input = unlines $ "begin":addSemicolon (map show input) ++ ["end"]
     where addSemicolon (x:xs@(_:_)) = (x ++ ";") : addSemicolon xs
           addSemicolon xs           = xs
-          (beginMark,endMark) = if simpleFormat params then ("begin","end") else ("{","}")