diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am
index 94d1855fb..2835ea04e 100644
--- a/src/misc/Makefile.am
+++ b/src/misc/Makefile.am
@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+## Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 ## Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -32,7 +32,6 @@ DISTCLEANFILES = _config.h
 misc_HEADERS = \
   bareword.hh \
   bddlt.hh \
-  bddop.hh \
   bitvect.hh \
   casts.hh \
   common.hh \
@@ -59,7 +58,6 @@ misc_HEADERS = \
 noinst_LTLIBRARIES = libmisc.la
 libmisc_la_SOURCES = \
   bareword.cc \
-  bddop.cc \
   bitvect.cc \
   escape.cc \
   formater.cc \
diff --git a/src/misc/bddop.cc b/src/misc/bddop.cc
deleted file mode 100644
index 0fefa075d..000000000
--- a/src/misc/bddop.cc
+++ /dev/null
@@ -1,65 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 3 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-#include "config.h"
-#include <cassert>
-#include "bddop.hh"
-
-namespace spot
-{
-  bdd
-  compute_all_acceptance_conditions(bdd neg_acceptance_conditions)
-  {
-    bdd all = bddfalse;
-
-    // Build all_acceptance_conditions_ from neg_acceptance_conditions_
-    // I.e., transform !A & !B & !C into
-    //        A & !B & !C
-    //     + !A &  B & !C
-    //     + !A & !B &  C
-    bdd cur = neg_acceptance_conditions;
-    while (cur != bddtrue)
-    {
-      assert(cur != bddfalse);
-
-      bdd v = bdd_ithvar(bdd_var(cur));
-      all |= v & bdd_exist(neg_acceptance_conditions, v);
-
-      assert(bdd_high(cur) != bddtrue);
-      cur = bdd_low(cur);
-    }
-
-    return all;
-  }
-
-  bdd
-  compute_neg_acceptance_conditions(bdd all_acceptance_conditions)
-  {
-    bdd cur = bdd_support(all_acceptance_conditions);
-    bdd neg = bddtrue;
-    while (cur != bddtrue)
-      {
-	neg &= bdd_nithvar(bdd_var(cur));
-	assert(bdd_low(cur) != bddtrue);
-	cur = bdd_high(cur);
-      }
-    return neg;
-  }
-
-}
diff --git a/src/misc/bddop.hh b/src/misc/bddop.hh
deleted file mode 100644
index 213949dcf..000000000
--- a/src/misc/bddop.hh
+++ /dev/null
@@ -1,39 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2013, 2014 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
-//
-// This file is part of Spot, a model checking library.
-//
-// Spot is free software; you can redistribute it and/or modify it
-// under the terms of the GNU General Public License as published by
-// the Free Software Foundation; either version 3 of the License, or
-// (at your option) any later version.
-//
-// Spot is distributed in the hope that it will be useful, but WITHOUT
-// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
-// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
-// License for more details.
-//
-// You should have received a copy of the GNU General Public License
-// along with this program.  If not, see <http://www.gnu.org/licenses/>.
-
-#ifndef SPOT_MISC_BDDOP_HH
-# define SPOT_MISC_BDDOP_HH
-
-#include "common.hh"
-#include <bddx.h>
-
-namespace spot
-{
-  /// \brief Compute all acceptance conditions from all neg acceptance
-  /// conditions.
-  SPOT_API bdd
-  compute_all_acceptance_conditions(bdd neg_acceptance_conditions);
-
-  /// \brief Compute neg acceptance conditions from all acceptance
-  /// conditions.
-  SPOT_API bdd
-  compute_neg_acceptance_conditions(bdd all_acceptance_conditions);
-}
-
-#endif // SPOT_MISC_BDDOP_HH
diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc
index c4b08f3bc..c313d8e84 100644
--- a/src/ta/taexplicit.cc
+++ b/src/ta/taexplicit.cc
@@ -30,7 +30,6 @@
 #include "ltlast/constant.hh"
 #include "taexplicit.hh"
 #include "tgba/formula2bdd.hh"
-#include "misc/bddop.hh"
 #include <cassert>
 #include "ltlvisit/tostring.hh"
 
diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc
index 42ee7c6b9..77ec99f86 100644
--- a/src/ta/tgtaexplicit.cc
+++ b/src/ta/tgtaexplicit.cc
@@ -21,7 +21,6 @@
 #include "ltlast/constant.hh"
 #include "tgtaexplicit.hh"
 #include "tgba/formula2bdd.hh"
-#include "misc/bddop.hh"
 #include "ltlvisit/tostring.hh"
 
 #include "tgba/bddprint.hh"
diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc
index 0df289977..cd4cedf97 100644
--- a/src/taalgos/tgba2ta.cc
+++ b/src/taalgos/tgba2ta.cc
@@ -29,7 +29,6 @@
 #include "ltlast/atomic_prop.hh"
 #include "ltlast/constant.hh"
 #include "tgba/formula2bdd.hh"
-#include "misc/bddop.hh"
 #include <cassert>
 #include "ltlvisit/tostring.hh"
 #include <iostream>
diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc
index f0bbf0419..2df276d03 100644
--- a/src/tgba/taatgba.cc
+++ b/src/tgba/taatgba.cc
@@ -24,7 +24,6 @@
 #include "tgba/formula2bdd.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/clone.hh"
-#include "misc/bddop.hh"
 #include "taatgba.hh"
 
 namespace spot
diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh
index f5c6182f4..9f0bcf7a8 100644
--- a/src/tgba/tgbagraph.hh
+++ b/src/tgba/tgbagraph.hh
@@ -26,7 +26,6 @@
 #include "tgba/bdddict.hh"
 #include "tgba/tgba.hh"
 #include "tgbaalgos/dupexp.hh"
-#include "misc/bddop.hh"
 #include <sstream>
 
 namespace spot