diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,44 +1,82 @@
+# This file has been generated -- see https://github.com/hvr/multi-ghc-travis
+language: c
 sudo: false
 
+cache:
+  directories:
+    - $HOME/.cabsnap
+    - $HOME/.cabal/packages
+
+before_cache:
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.tar
+
 matrix:
   include:
-    - env: CABALVER=1.22 GHCVER=7.10.2
-      addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.2],sources: [hvr-ghc]}}
+    - env: CABALVER=1.22 GHCVER=7.10.3
+      compiler: ": #GHC 7.10.3"
+      addons: {apt: {packages: [cabal-install-1.22,ghc-7.10.3], sources: [hvr-ghc]}}
     - env: CABALVER=head GHCVER=head
-      addons: {apt: {packages: [cabal-install-head,ghc-head],  sources: [hvr-ghc]}}
+      compiler: ": #GHC head"
+      addons: {apt: {packages: [cabal-install-head,ghc-head], sources: [hvr-ghc]}}
 
   allow_failures:
-   - env: CABALVER=head GHCVER=head
+    - env: CABALVER=head GHCVER=head
 
 before_install:
+ - unset CC
  - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
 
 install:
  - cabal --version
  - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"
- - travis_retry cabal update
- - cabal install --only-dependencies --enable-tests --enable-benchmarks
+ - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];
+   then
+     zcat $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz >
+          $HOME/.cabal/packages/hackage.haskell.org/00-index.tar;
+   fi
+ - travis_retry cabal update -v
+ - sed -i 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config
+ - cabal install --only-dependencies --enable-tests --enable-benchmarks --dry -v > installplan.txt
+ - sed -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
 
-# Here starts the actual work to be performed for the package under
-# test; any command which exits with a non-zero exit code causes the
-# build to fail.
+# check whether current requested install-plan matches cached package-db snapshot
+ - if diff -u installplan.txt $HOME/.cabsnap/installplan.txt;
+   then
+     echo "cabal build-cache HIT";
+     rm -rfv .ghc;
+     cp -a $HOME/.cabsnap/ghc $HOME/.ghc;
+     cp -a $HOME/.cabsnap/lib $HOME/.cabsnap/share $HOME/.cabsnap/bin $HOME/.cabal/;
+   else
+     echo "cabal build-cache MISS";
+     rm -rf $HOME/.cabsnap;
+     mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
+     cabal install --only-dependencies --enable-tests --enable-benchmarks;
+   fi
 
+# snapshot package-db on cache miss
+ - if [ ! -d $HOME/.cabsnap ];
+   then
+      echo "snapshotting package-db to build-cache";
+      mkdir $HOME/.cabsnap;
+      cp -a $HOME/.ghc $HOME/.cabsnap/ghc;
+      cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin installplan.txt $HOME/.cabsnap/;
+   fi
+
+# Here starts the actual work to be performed for the package under test;
+# any command which exits with a non-zero exit code causes the build to fail.
 script:
- - cabal configure --enable-tests -v2  # -v2 provides useful information for debugging
+ - if [ -f configure.ac ]; then autoreconf -i; fi
+ - cabal configure --enable-tests --enable-benchmarks -v2  # -v2 provides useful information for debugging
  - cabal build   # this builds all libraries and executables (including tests/benchmarks)
  - cabal test
- # - cabal check
+# - cabal check
  - cabal sdist   # tests that a source-distribution can be generated
 
-# The following scriptlet checks that the resulting source distribution can be built & installed
- - export SRC_TGZ=$(cabal info . | awk '{print $2 ".tar.gz";exit}') ;
-   cd dist/;
-   if [ -f "$SRC_TGZ" ]; then
-      cabal install --force-reinstalls "$SRC_TGZ";
-   else
-      echo "expected '$SRC_TGZ' not found";
-      exit 1;
-   fi
+# Check that the resulting source distribution can be built & installed.
+# If there are no other `.tar.gz` files in `dist`, this can be even simpler:
+# `cabal install --force-reinstalls dist/*-*.tar.gz`
+ - SRC_TGZ=$(cabal info . | awk '{print $2;exit}').tar.gz &&
+   (cd dist && cabal install --force-reinstalls "$SRC_TGZ")
 
-after_script:
-  - cat dist/test/*.log
+# EOF
diff --git a/atp-haskell.cabal b/atp-haskell.cabal
--- a/atp-haskell.cabal
+++ b/atp-haskell.cabal
@@ -1,5 +1,5 @@
 Name:             atp-haskell
-Version:          1.9
+Version:          1.10
 Synopsis:         Translation from Ocaml to Haskell of John Harrison's ATP code
 Description:      This package is a liberal translation from OCaml to Haskell of
                   the automated theorem prover written in OCaml in
@@ -15,6 +15,7 @@
 Cabal-version:    >= 1.9
 Build-Type:       Simple
 Extra-Source-Files: tests/Extra.hs, .travis.yml, .ghci
+Tested-With:      GHC == 7.10.3, GHC == 7.11.*
 
 Source-Repository head
   type: git
diff --git a/src/Data/Logic/ATP/Unif.hs b/src/Data/Logic/ATP/Unif.hs
--- a/src/Data/Logic/ATP/Unif.hs
+++ b/src/Data/Logic/ATP/Unif.hs
@@ -52,36 +52,38 @@
 -- EqualityT a) b)@.
 class (IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify a where
     type UTermOf a
-    unify :: a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) Failing ()
+    unify :: Monad m => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m ()
 
-unify_terms :: (IsTerm term, v ~ TVarOf term) => [(term,term)] -> StateT (Map v term) Failing ()
+unify_terms :: (IsTerm term, v ~ TVarOf term, Monad m) =>
+               [(term,term)] -> StateT (Map v term) m ()
 unify_terms = mapM_ (uncurry unify_term_pair)
 
-unify_term_pair :: forall term v f. (IsTerm term, v ~ TVarOf term, f ~ FunOf term) =>
-                   term -> term -> StateT (Map v term) Failing ()
+unify_term_pair :: forall term v f m.
+                   (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) =>
+                   term -> term -> StateT (Map v term) m ()
 unify_term_pair a b =
     foldTerm (vr b) (\ f fargs -> foldTerm (vr a) (fn f fargs) b) a
     where
-      vr :: term -> v -> StateT (Map v term) Failing ()
+      vr :: term -> v -> StateT (Map v term) m ()
       vr t x =
           (Map.lookup x <$> get) >>=
           maybe (istriv x t >>= bool (modify (Map.insert x t)) (return ()))
                 (\y -> unify_term_pair y t)
-      fn :: f -> [term] -> f -> [term] -> StateT (Map v term) Failing ()
+      fn :: f -> [term] -> f -> [term] -> StateT (Map v term) m ()
       fn f fargs g gargs =
           if f == g && length fargs == length gargs
           then mapM_ (uncurry unify_term_pair) (zip fargs gargs)
           else fail "impossible unification"
 
-istriv :: forall term v. (IsTerm term, v ~ TVarOf term) =>
-          v -> term -> StateT (Map v term) Failing Bool
+istriv :: forall term v m. (IsTerm term, v ~ TVarOf term, Monad m) =>
+          v -> term -> StateT (Map v term) m Bool
 istriv x t =
     foldTerm vr fn t
     where
-      -- vr :: v -> StateT (Map v term) Failing Bool
+      vr :: v -> StateT (Map v term) m Bool
       vr y | x == y = return True
       vr y = (Map.lookup y <$> get) >>= maybe (return False) (istriv x)
-      -- fn :: f -> [term] -> StateT (Map v term) Failing Bool
+      fn :: f -> [term] -> StateT (Map v term) m Bool
       fn _ args = mapM (istriv x) args >>= bool (return False) (fail "cyclic") . or
 
 -- | Solve to obtain a single instantiation.
@@ -92,13 +94,13 @@
     where env' = Map.map (tsubst env) env
 
 -- | Unification reaching a final solved form (often this isn't needed).
-fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term) =>
-             [(term,term)] -> Failing (Map v term)
+fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) =>
+             [(term,term)] -> m (Map v term)
 fullunify eqs = solve <$> execStateT (unify_terms eqs) Map.empty
 
 -- | Examples.
-unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term) =>
-                   [(term, term)] -> Failing [(term, term)]
+unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) =>
+                   [(term, term)] -> m [(term, term)]
 unify_and_apply eqs =
     fullunify eqs >>= \i -> return $ List.map (\ (t1, t2) -> (tsubst i t1, tsubst i t2)) eqs
 
@@ -108,8 +110,8 @@
 -- who cares.
 unify_literals :: (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
                    JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2,
-                   Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) =>
-                  lit1 -> lit2 -> StateT (Map v term) Failing ()
+                   Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, Monad m) =>
+                  lit1 -> lit2 -> StateT (Map v term) m ()
 unify_literals f1 f2 =
     fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2)
     where
@@ -120,21 +122,21 @@
 
 unify_atoms :: (JustApply atom1, term ~ TermOf atom1,
                 JustApply atom2, term ~ TermOf atom2,
-                v ~ TVarOf term, PredOf atom1 ~ PredOf atom2) =>
-               (atom1, atom2) -> StateT (Map v term) Failing ()
+                v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, Monad m) =>
+               (atom1, atom2) -> StateT (Map v term) m ()
 unify_atoms (a1, a2) =
     maybe (fail "unify_atoms") id (zipApplys (\_ tpairs -> Just (unify_terms tpairs)) a1 a2)
 
 unify_atoms_eq :: (HasEquate atom1, term ~ TermOf atom1,
                    HasEquate atom2, term ~ TermOf atom2,
-                   PredOf atom1 ~ PredOf atom2, v ~ TVarOf term) =>
-                  atom1 -> atom2 -> StateT (Map v term) Failing ()
+                   PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, Monad m) =>
+                  atom1 -> atom2 -> StateT (Map v term) m ()
 unify_atoms_eq a1 a2 =
     maybe (fail "unify_atoms") id (zipEquates (\l1 r1 l2 r2 -> Just (unify_terms [(l1, l2), (r1, r2)]))
                                               (\_ tpairs -> Just (unify_terms tpairs))
                                               a1 a2)
 
---unify_and_apply' :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => [(term, term)] -> Failing [(term, term)]
+--unify_and_apply' :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term, Monad m) => [(term, term)] -> m [(term, term)]
 --unify_and_apply' eqs =
 --    mapM app eqs
 --        where