diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am
index 4928a16e7..a60ae67ad 100644
--- a/src/tgba/Makefile.am
+++ b/src/tgba/Makefile.am
@@ -1,7 +1,8 @@
-## Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
-## Développement de l'Epita (LRDE).
+## -*- coding: utf-8 -*-
+## Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et
+## Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
-## département Systèmes Répartis Coopératifs (SRC), Université Pierre
+## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
 ##
 ## This file is part of Spot, a model checking library.
@@ -20,7 +21,7 @@
 ## along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
-AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS) $(VISIBILITY_CXXFLAGS)
 
 tgbadir = $(pkgincludedir)/tgba
 
diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh
index 63a63a1eb..e43e7b89d 100644
--- a/src/tgba/bdddict.hh
+++ b/src/tgba/bdddict.hh
@@ -54,7 +54,7 @@ namespace spot
   /// unregister_all_my_variables(), giving the same pointer.
   /// Variables can also by unregistered one by one using
   /// unregister_variable().
-  class bdd_dict
+  class SPOT_API bdd_dict
   {
     bdd_dict_priv* priv_;
   public:
diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh
index 8659ebd40..889f4b834 100644
--- a/src/tgba/bddprint.hh
+++ b/src/tgba/bddprint.hh
@@ -37,8 +37,8 @@ namespace spot
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
-  std::ostream& bdd_print_sat(std::ostream& os,
-			      const bdd_dict* dict, bdd b);
+  SPOT_API std::ostream&
+  bdd_print_sat(std::ostream& os, const bdd_dict* dict, bdd b);
 
   /// \brief Format a BDD as a list of literals.
   ///
@@ -46,7 +46,8 @@ namespace spot
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
-  std::string bdd_format_sat(const bdd_dict* dict, bdd b);
+  SPOT_API std::string
+  bdd_format_sat(const bdd_dict* dict, bdd b);
 
   /// \brief Print a BDD as a list of acceptance conditions.
   ///
@@ -55,8 +56,8 @@ namespace spot
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
-  std::ostream& bdd_print_acc(std::ostream& os,
-			      const bdd_dict* dict, bdd b);
+  SPOT_API std::ostream&
+  bdd_print_acc(std::ostream& os, const bdd_dict* dict, bdd b);
 
   /// \brief Print a BDD as a set of acceptance conditions.
   ///
@@ -65,8 +66,8 @@ namespace spot
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
-  std::ostream& bdd_print_accset(std::ostream& os,
-				 const bdd_dict* dict, bdd b);
+  SPOT_API std::ostream&
+  bdd_print_accset(std::ostream& os, const bdd_dict* dict, bdd b);
 
   /// \brief Format a BDD as a set of acceptance conditions.
   ///
@@ -74,55 +75,60 @@ namespace spot
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
-  std::string bdd_format_accset(const bdd_dict* dict, bdd b);
+  SPOT_API std::string
+  bdd_format_accset(const bdd_dict* dict, bdd b);
 
   /// \brief Print a BDD as a set.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
-  std::ostream& bdd_print_set(std::ostream& os,
-			      const bdd_dict* dict, bdd b);
+  SPOT_API std::ostream&
+  bdd_print_set(std::ostream& os, const bdd_dict* dict, bdd b);
+
   /// \brief Format a BDD as a set.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
-  std::string bdd_format_set(const bdd_dict* dict, bdd b);
+  SPOT_API std::string
+  bdd_format_set(const bdd_dict* dict, bdd b);
 
   /// \brief Print a BDD as a formula.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
-  std::ostream& bdd_print_formula(std::ostream& os,
-				  const bdd_dict* dict, bdd b);
+  SPOT_API std::ostream&
+  bdd_print_formula(std::ostream& os, const bdd_dict* dict, bdd b);
+
   /// \brief Format a BDD as a formula.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
-  std::string bdd_format_formula(const bdd_dict* dict, bdd b);
+  SPOT_API std::string
+  bdd_format_formula(const bdd_dict* dict, bdd b);
 
   /// \brief Print a BDD as a diagram in dotty format.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
-  std::ostream& bdd_print_dot(std::ostream& os,
-			      const bdd_dict* dict, bdd b);
+  SPOT_API std::ostream&
+  bdd_print_dot(std::ostream& os, const bdd_dict* dict, bdd b);
 
   /// \brief Print a BDD as a table.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
-  std::ostream& bdd_print_table(std::ostream& os,
-				const bdd_dict* dict, bdd b);
+  SPOT_API std::ostream&
+  bdd_print_table(std::ostream& os, const bdd_dict* dict, bdd b);
 
   /// \brief Enable UTF-8 output for bdd printers.
-  void enable_utf8();
+  SPOT_API void enable_utf8();
 
 
   /// \brief Format a BDD as an irredundant sum of product.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
-  std::string
+  SPOT_API std::string
   bdd_format_isop(const bdd_dict* dict, bdd b);
 
 
@@ -130,7 +136,7 @@ namespace spot
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
-  std::ostream&
+  SPOT_API std::ostream&
   bdd_print_isop(std::ostream& os, const bdd_dict* dict, bdd b);
 
 }
diff --git a/src/tgba/formula2bdd.hh b/src/tgba/formula2bdd.hh
index b3d746e05..f8820fb9b 100644
--- a/src/tgba/formula2bdd.hh
+++ b/src/tgba/formula2bdd.hh
@@ -24,7 +24,6 @@
 # define SPOT_TGBA_FORMULA2BDD_HH
 
 # include "bdddict.hh"
-# include "ltlast/formula.hh"
 
 namespace spot
 {
@@ -39,7 +38,8 @@ namespace spot
   /// passing it right away to bdd_to_formula(), you should not forget
   /// to unregister the variables that have been registered for \a
   /// for_me.  See bdd_dict::unregister_all_my_variables().
-  bdd formula_to_bdd(const ltl::formula* f, bdd_dict* d, void* for_me);
+  SPOT_API bdd
+  formula_to_bdd(const ltl::formula* f, bdd_dict* d, void* for_me);
 
   /// \brief Convert a BDD into a formula.
   ///
@@ -49,7 +49,8 @@ namespace spot
   /// formulas, and all the BDD variables used in \a f should have
   /// been registered in \a d.  Although the result has type
   /// ltl::formula*, it obviously does not use any temporal operator.
-  const ltl::formula* bdd_to_formula(bdd f, const bdd_dict* d);
+  SPOT_API const
+  ltl::formula* bdd_to_formula(bdd f, const bdd_dict* d);
 }
 
 #endif // SPOT_TGBA_FORMULA2BDD_HH
diff --git a/src/tgba/futurecondcol.hh b/src/tgba/futurecondcol.hh
index c66a12aba..4d2ebcb76 100644
--- a/src/tgba/futurecondcol.hh
+++ b/src/tgba/futurecondcol.hh
@@ -1,4 +1,6 @@
-// Copyright (C) 2009  Laboratoire de recherche et développement de l'Epita.
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2013 Laboratoire de recherche et développement
+// de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -32,7 +34,7 @@ namespace spot
   /// This new method returns a set of conditions that can be
   /// seen on a transitions accessible (maybe indirectly) from
   /// the given state.
-  class future_conditions_collector : public tgba_scc
+  class SPOT_API future_conditions_collector : public tgba_scc
   {
   public:
     typedef scc_map::cond_set cond_set;
diff --git a/src/tgba/public.hh b/src/tgba/public.hh
index ff7ceeb43..e1b9cd8e8 100644
--- a/src/tgba/public.hh
+++ b/src/tgba/public.hh
@@ -1,5 +1,8 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 Laboratoire de Recherche et Developpement de
+// l'Epita (LRDE).
 // Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -20,6 +23,13 @@
 #ifndef SPOT_TGBA_PUBLIC_HH
 # define SPOT_TGBA_PUBLIC_HH
 
+// This file should not exist.
+#if __GNUC__
+#ifndef SKIP_DEPRECATED_WARNING
+#warning This file is deprecated.  Include tgba.hh or what you need.
+#endif
+#endif
+
 # include "tgba.hh"
 # include "tgbabddconcrete.hh"
 # include "tgbabddconcreteproduct.hh"
diff --git a/src/tgba/state.hh b/src/tgba/state.hh
index ca363be02..7d87ae2ab 100644
--- a/src/tgba/state.hh
+++ b/src/tgba/state.hh
@@ -23,6 +23,7 @@
 #ifndef SPOT_TGBA_STATE_HH
 # define SPOT_TGBA_STATE_HH
 
+#include "misc/common.hh"
 #include <cstddef>
 #include <bdd.h>
 #include <cassert>
@@ -35,7 +36,7 @@ namespace spot
 
   /// \ingroup tgba_essentials
   /// \brief Abstract class for states.
-  class state
+  class SPOT_API state
   {
   public:
     /// \brief Compares two states (that come from the same automaton).
diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh
index 2edb42b36..355feac98 100644
--- a/src/tgba/statebdd.hh
+++ b/src/tgba/statebdd.hh
@@ -1,5 +1,8 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 Laboratoire de Recherche et Développement de
+// l'Epita.
 // Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -27,7 +30,7 @@ namespace spot
 {
   /// A state whose representation is a BDD.
   /// \ingroup tgba_representation
-  class state_bdd: public state
+  class SPOT_API state_bdd: public state
   {
   public:
     state_bdd(bdd s)
diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh
index 2f592fc23..880ba11f5 100644
--- a/src/tgba/succiter.hh
+++ b/src/tgba/succiter.hh
@@ -1,7 +1,8 @@
+// -*- coding: utf-8 -*-
 // Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de
 // l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -34,7 +35,7 @@ namespace spot
   /// transition labels.  Because transitions are never explicitely
   /// encoded, labels (conditions and acceptance conditions) can only
   /// be queried while iterating over the successors.
-  class tgba_succ_iterator
+  class SPOT_API tgba_succ_iterator
   {
   public:
     virtual
diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh
index 29136b8be..7b1a8b08f 100644
--- a/src/tgba/succiterconcrete.hh
+++ b/src/tgba/succiterconcrete.hh
@@ -1,5 +1,8 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 Laboratoire de Recherche et Developpement de
+// l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -28,7 +31,8 @@ namespace spot
 {
   /// A concrete iterator over successors of a TGBA state.
   /// \ingroup tgba_representation
-  class tgba_succ_iterator_concrete: public tgba_succ_iterator
+  class SPOT_API tgba_succ_iterator_concrete:
+    public tgba_succ_iterator
   {
   public:
     /// \brief Build a spot::tgba_succ_iterator_concrete.
diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh
index 2cc2cfad2..59ee73991 100644
--- a/src/tgba/taatgba.hh
+++ b/src/tgba/taatgba.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et
+// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -32,7 +32,7 @@ namespace spot
 {
   /// \brief A self-loop Transition-based Alternating Automaton (TAA)
   /// which is seen as a TGBA (abstract class, see below).
-  class taa_tgba : public tgba
+  class SPOT_API taa_tgba : public tgba
   {
   public:
     taa_tgba(bdd_dict* dict);
@@ -83,7 +83,7 @@ namespace spot
   };
 
   /// Set of states deriving from spot::state.
-  class state_set : public spot::state
+  class SPOT_API state_set : public spot::state
   {
   public:
     state_set(const taa_tgba::state_set* s, bool delete_me = false)
@@ -107,7 +107,7 @@ namespace spot
     bool delete_me_;
   };
 
-  class taa_succ_iterator : public tgba_succ_iterator
+  class SPOT_API taa_succ_iterator : public tgba_succ_iterator
   {
   public:
     taa_succ_iterator(const taa_tgba::state_set* s, bdd all_acc);
@@ -152,7 +152,7 @@ namespace spot
   /// A taa_tgba instance with states labeled by a given type.
   /// Still an abstract class, see below.
   template<typename label, typename label_hash>
-  class taa_tgba_labelled : public taa_tgba
+  class SPOT_API taa_tgba_labelled : public taa_tgba
   {
   public:
     taa_tgba_labelled(bdd_dict* dict) : taa_tgba(dict) {};
@@ -324,7 +324,7 @@ namespace spot
     }
   };
 
-  class taa_tgba_string :
+  class SPOT_API taa_tgba_string :
     public taa_tgba_labelled<std::string, string_hash>
   {
   public:
@@ -336,7 +336,7 @@ namespace spot
     virtual std::string clone_if(const std::string& label) const;
   };
 
-  class taa_tgba_formula :
+  class SPOT_API taa_tgba_formula :
     public taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>
   {
   public:
diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh
index 399c00cb3..3fd620cb6 100644
--- a/src/tgba/tgba.hh
+++ b/src/tgba/tgba.hh
@@ -64,7 +64,7 @@ namespace spot
   /// we never represent transitions!  Transition informations are
   /// obtained by querying the iterator over the successors of
   /// a state.
-  class tgba
+  class SPOT_API tgba
   {
   protected:
     tgba();
diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh
index 0962f12df..227a1935a 100644
--- a/src/tgba/tgbabddconcrete.hh
+++ b/src/tgba/tgbabddconcrete.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2011 Laboratoire de Recherche et Développement
+// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -31,7 +31,7 @@ namespace spot
 {
   /// \ingroup tgba_representation
   /// \brief A concrete spot::tgba implemented using BDDs.
-  class tgba_bdd_concrete: public tgba
+  class SPOT_API tgba_bdd_concrete: public tgba
   {
   public:
     /// \brief Construct a tgba_bdd_concrete with unknown initial state.
diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh
index 9b4ba488a..d3c74926d 100644
--- a/src/tgba/tgbabddconcretefactory.hh
+++ b/src/tgba/tgbabddconcretefactory.hh
@@ -1,7 +1,8 @@
-// Copyright (C) 2008 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -29,7 +30,7 @@
 namespace spot
 {
   /// Helper class to build a spot::tgba_bdd_concrete object.
-  class tgba_bdd_concrete_factory: public tgba_bdd_factory
+  class SPOT_API tgba_bdd_concrete_factory: public tgba_bdd_factory
   {
   public:
     tgba_bdd_concrete_factory(bdd_dict* dict);
diff --git a/src/tgba/tgbabddconcreteproduct.hh b/src/tgba/tgbabddconcreteproduct.hh
index f6ae5687d..837baedd3 100644
--- a/src/tgba/tgbabddconcreteproduct.hh
+++ b/src/tgba/tgbabddconcreteproduct.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2013  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -29,7 +29,7 @@ namespace spot
   ///
   /// This function builds the resulting product as another
   /// spot::tgba_bdd_concrete automaton.
-  tgba_bdd_concrete*
+  SPOT_API tgba_bdd_concrete*
   product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right);
 }
 
diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh
index 759c60294..c2776a891 100644
--- a/src/tgba/tgbabddcoredata.hh
+++ b/src/tgba/tgbabddcoredata.hh
@@ -1,7 +1,8 @@
-// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -28,7 +29,7 @@
 namespace spot
 {
   /// Core data for a TGBA encoded using BDDs.
-  struct tgba_bdd_core_data
+  struct SPOT_API tgba_bdd_core_data
   {
     /// \brief encodes the transition relation of the TGBA.
     ///
@@ -42,7 +43,7 @@ namespace spot
     /// \brief encodes the acceptance conditions
     ///
     /// <tt>a U b</tt>, or <tt>F b</tt>, both imply that \c b should
-    /// be verified eventually.  We encode this with generalized Büchi
+    /// be verified eventually.  We encode this with generalized Büchi
     /// acceptating conditions.  An acceptance set, called
     /// <tt>Acc[b]</tt>, hold all the state that do not promise to
     /// verify \c b eventually.  (I.e., all the states that contain \c
diff --git a/src/tgba/tgbabddfactory.hh b/src/tgba/tgbabddfactory.hh
index 80c639385..5799d9c25 100644
--- a/src/tgba/tgbabddfactory.hh
+++ b/src/tgba/tgbabddfactory.hh
@@ -1,5 +1,8 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 Laboratoire de Recherche et Developpement de
+// l'Epita (LRDE).
 // Copyright (C) 2003, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
@@ -28,7 +31,7 @@ namespace spot
   ///
   /// A spot::tgba_bdd_concrete can be constructed from anything that
   /// supplies core data and their associated dictionary.
-  class tgba_bdd_factory
+  class SPOT_API tgba_bdd_factory
   {
   public:
     virtual ~tgba_bdd_factory() {}
diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh
index 375891d7a..b6915aa10 100644
--- a/src/tgba/tgbaexplicit.hh
+++ b/src/tgba/tgbaexplicit.hh
@@ -38,7 +38,7 @@ namespace spot
 {
   // How to destroy the label of a state.
   template<typename T>
-  struct destroy_key
+  struct SPOT_API destroy_key
   {
     void destroy(T t)
     {
@@ -47,7 +47,7 @@ namespace spot
   };
 
   template<>
-  struct destroy_key<const ltl::formula*>
+  struct SPOT_API destroy_key<const ltl::formula*>
   {
     void destroy(const ltl::formula* t)
     {
@@ -58,7 +58,7 @@ namespace spot
   /// States used by spot::explicit_graph implementation
   /// \ingroup tgba_representation
   template<typename Label, typename label_hash>
-  class state_explicit: public spot::state
+  class SPOT_API state_explicit: public spot::state
   {
   public:
     state_explicit()
@@ -133,7 +133,7 @@ namespace spot
 
   /// States labeled by an int
   /// \ingroup tgba_representation
-  class state_explicit_number:
+  class SPOT_API state_explicit_number:
     public state_explicit<int, identity_hash<int> >
   {
   public:
@@ -152,7 +152,7 @@ namespace spot
 
   /// States labeled by a string
   /// \ingroup tgba_representation
-  class state_explicit_string:
+  class SPOT_API state_explicit_string:
     public state_explicit<std::string, string_hash>
   {
   public:
@@ -171,7 +171,7 @@ namespace spot
 
   /// States labeled by a formula
   /// \ingroup tgba_representation
-  class state_explicit_formula:
+  class SPOT_API state_explicit_formula:
     public state_explicit<const ltl::formula*, ltl::formula_ptr_hash>
   {
   public:
@@ -191,7 +191,8 @@ namespace spot
   /// Successor iterators used by spot::tgba_explicit.
   /// \ingroup tgba_representation
   template<typename State>
-  class tgba_explicit_succ_iterator: public tgba_succ_iterator
+  class SPOT_API tgba_explicit_succ_iterator:
+    public tgba_succ_iterator
   {
   public:
     tgba_explicit_succ_iterator(const State* start,
@@ -251,7 +252,7 @@ namespace spot
   /// Graph implementation for explicit automaton
   /// \ingroup tgba_representation
   template<typename State, typename Type>
-  class explicit_graph: public Type
+  class SPOT_API explicit_graph: public Type
   {
   public:
     typedef typename State::label_t label_t;
@@ -694,7 +695,8 @@ namespace spot
   };
 
   template <typename State>
-  class tgba_explicit: public explicit_graph<State, tgba>
+  class SPOT_API tgba_explicit:
+    public explicit_graph<State, tgba>
   {
   public:
     tgba_explicit(bdd_dict* dict): explicit_graph<State, tgba>(dict)
@@ -712,7 +714,8 @@ namespace spot
   };
 
   template <typename State>
-  class sba_explicit: public explicit_graph<State, sba>
+  class SPOT_API sba_explicit:
+    public explicit_graph<State, sba>
   {
   public:
     sba_explicit(bdd_dict* dict): explicit_graph<State, sba>(dict)
@@ -752,7 +755,7 @@ namespace spot
   /// Configuration of graph automata
   /// \ingroup tgba_representation
   template<class graph, typename Type>
-  class explicit_conf: public graph
+  class SPOT_API explicit_conf: public graph
   {
   public:
     explicit_conf(bdd_dict* d): graph(d)
@@ -769,7 +772,7 @@ namespace spot
   };
 
   template<class graph>
-  class explicit_conf<graph, state_explicit_string>: public graph
+  class SPOT_API explicit_conf<graph, state_explicit_string>: public graph
   {
   public:
     explicit_conf(bdd_dict* d): graph(d)
@@ -784,7 +787,7 @@ namespace spot
   };
 
   template<class graph>
-  class explicit_conf<graph, state_explicit_formula>: public graph
+  class SPOT_API explicit_conf<graph, state_explicit_formula>: public graph
   {
   public:
     explicit_conf(bdd_dict* d): graph(d)
diff --git a/src/tgba/tgbakvcomplement.hh b/src/tgba/tgbakvcomplement.hh
index 7b2032c2b..8a1f429a2 100644
--- a/src/tgba/tgbakvcomplement.hh
+++ b/src/tgba/tgbakvcomplement.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
+// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -27,7 +27,7 @@
 
 namespace spot
 {
-  class bdd_ordered
+  class SPOT_API bdd_ordered
   {
   public:
     bdd_ordered()
@@ -83,7 +83,7 @@ namespace spot
   /// The construction is done on-the-fly, by the
   /// \c tgba_kv_complement_succ_iterator class.
   /// \see tgba_kv_complement_succ_iterator
-  class tgba_kv_complement : public tgba
+  class SPOT_API tgba_kv_complement : public tgba
   {
   public:
     tgba_kv_complement(const tgba* a);
diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh
index 736f75fe7..1647969f6 100644
--- a/src/tgba/tgbaproduct.hh
+++ b/src/tgba/tgbaproduct.hh
@@ -1,8 +1,9 @@
-// Copyright (C) 2011 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
-// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -33,7 +34,7 @@ namespace spot
   ///
   /// This state is in fact a pair of state: the state from the left
   /// automaton and that of the right.
-  class state_product : public state
+  class SPOT_API state_product : public state
   {
   public:
     /// \brief Constructor
@@ -77,7 +78,7 @@ namespace spot
 
 
   /// \brief A lazy product.  (States are computed on the fly.)
-  class tgba_product: public tgba
+  class SPOT_API tgba_product: public tgba
   {
   public:
     /// \brief Constructor.
@@ -130,7 +131,7 @@ namespace spot
   };
 
   /// \brief A lazy product with different initial states.
-  class tgba_product_init: public tgba_product
+  class SPOT_API tgba_product_init: public tgba_product
   {
   public:
     tgba_product_init(const tgba* left, const tgba* right,
diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh
index 54c083c98..16ed2f664 100644
--- a/src/tgba/tgbasafracomplement.hh
+++ b/src/tgba/tgbasafracomplement.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2010, 2011, 2013 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -20,7 +21,7 @@
 # define SPOT_TGBA_TGBASAFRACOMPLEMENT_HH
 
 # include <vector>
-# include "tgba/tgba.hh"
+# include "tgba.hh"
 
 #ifndef TRANSFORM_TO_TBA
 # define TRANSFORM_TO_TBA 0
@@ -40,13 +41,13 @@ namespace spot
   /// 2. Interpreting this deterministic Rabin automaton as a
   ///    deterministic Streett will produce a complemented automaton.
   /// 3. Then we use a transformation from deterministic Streett
-  ///    automaton to nondeterministic Büchi automaton.
+  ///    automaton to nondeterministic Büchi automaton.
   ///
   ///  Safra construction is done in \a tgba_complement, the transformation
   ///  is done on-the-fly when successors are called.
   ///
   /// \sa safra_determinisation, tgba_safra_complement::succ_iter.
-  class tgba_safra_complement : public tgba
+  class SPOT_API tgba_safra_complement : public tgba
   {
   public:
     tgba_safra_complement(const tgba* a);
@@ -89,10 +90,9 @@ namespace spot
   /// \brief Produce a dot output of the Safra automaton associated
   /// to \a a.
   ///
-  /// @param a The \c tgba_safra_complement with an intermediate Safra
+  /// \param a The \c tgba_safra_complement with an intermediate Safra
   /// automaton to display
-  ///
-  void display_safra(const tgba_safra_complement* a);
+  void SPOT_API display_safra(const tgba_safra_complement* a);
 }
 
 #endif  // SPOT_TGBA_TGBASAFRACOMPLEMENT_HH
diff --git a/src/tgba/tgbascc.hh b/src/tgba/tgbascc.hh
index 7c4ffaa07..f6b47b174 100644
--- a/src/tgba/tgbascc.hh
+++ b/src/tgba/tgbascc.hh
@@ -1,4 +1,6 @@
-// Copyright (C) 2009  Laboratoire de recherche et développement de l'Epita.
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2013 Laboratoire de recherche et développement
+// de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -30,7 +32,7 @@ namespace spot
   ///
   /// This class is a spot::tgba wrapper that simply add a new method
   /// scc_of_state() to retrieve the number of a SCC a state belongs to.
-  class tgba_scc : public tgba
+  class SPOT_API tgba_scc : public tgba
   {
   public:
     /// \brief Create a tgba_scc wrapper for \a aut.
diff --git a/src/tgba/tgbasgba.hh b/src/tgba/tgbasgba.hh
index 92a2a804c..7e3affa25 100644
--- a/src/tgba/tgbasgba.hh
+++ b/src/tgba/tgbasgba.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -32,7 +32,7 @@ namespace spot
   /// This class acts as a proxy in front of a spot::tgba, that should
   /// label on states on-the-fly.  The result is still a spot::tgba,
   /// but acceptances conditions are also on states.
-  class tgba_sgba_proxy : public tgba
+  class SPOT_API tgba_sgba_proxy : public tgba
   {
   public:
     tgba_sgba_proxy(const tgba* a, bool no_zero_acc = true);
diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh
index 2ad68757c..4645edad4 100644
--- a/src/tgba/tgbatba.hh
+++ b/src/tgba/tgbatba.hh
@@ -49,7 +49,7 @@ namespace spot
   /// transitions.
   ///
   /// \see tgba_sba_proxy
-  class tgba_tba_proxy : public tgba
+  class SPOT_API tgba_tba_proxy : public tgba
   {
   public:
     tgba_tba_proxy(const tgba* a);
@@ -147,7 +147,7 @@ namespace spot
   /// one.
   ///
   /// \see degeneralize
-  class tgba_sba_proxy : public tgba_tba_proxy
+  class SPOT_API tgba_sba_proxy : public tgba_tba_proxy
   {
   public:
     tgba_sba_proxy(const tgba* a);
diff --git a/src/tgba/tgbaunion.hh b/src/tgba/tgbaunion.hh
index 63229bb22..39d13319f 100644
--- a/src/tgba/tgbaunion.hh
+++ b/src/tgba/tgbaunion.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -32,7 +33,7 @@ namespace spot
   /// If the first member is different from 0 and the second is 0,
   /// the state belongs to the right automaton.
   /// If both members are 0, the state is the initial state.
-  class state_union : public state
+  class SPOT_API state_union : public state
   {
   public:
     /// \brief Constructor
@@ -75,7 +76,7 @@ namespace spot
   };
 
    /// \brief Iterate over the successors of an union computed on the fly.
-  class tgba_succ_iterator_union: public tgba_succ_iterator
+  class SPOT_API tgba_succ_iterator_union: public tgba_succ_iterator
   {
   public:
     tgba_succ_iterator_union(tgba_succ_iterator* left,
@@ -107,7 +108,7 @@ namespace spot
   };
 
   /// \brief A lazy union.  (States are computed on the fly.)
-  class tgba_union: public tgba
+  class SPOT_API tgba_union: public tgba
   {
   public:
     /// \brief Constructor.
diff --git a/src/tgba/wdbacomp.hh b/src/tgba/wdbacomp.hh
index 0006b4987..52c078ca6 100644
--- a/src/tgba/wdbacomp.hh
+++ b/src/tgba/wdbacomp.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2011 Laboratoire de Recherche et Développement de
-// l'Epita.
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
+// de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -24,10 +25,11 @@
 namespace spot
 {
   /// \ingroup tgba_on_the_fly_algorithms
-  /// \brief Complement a weak deterministic Büchi automaton
-  /// \param aut a weak deterministic Büchi automaton to complement
+  /// \brief Complement a weak deterministic Büchi automaton
+  /// \param aut a weak deterministic Büchi automaton to complement
   /// \return a new automaton that recognizes the complement language
-  tgba* wdba_complement(const tgba* aut);
+  SPOT_API tgba*
+  wdba_complement(const tgba* aut);
 }
 
 #endif
diff --git a/src/tgbaalgos/cutscc.hh b/src/tgbaalgos/cutscc.hh
index 03dfb11ef..8ce4fd4bb 100644
--- a/src/tgbaalgos/cutscc.hh
+++ b/src/tgbaalgos/cutscc.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2009, 2013 Laboratoire de Recherche et Developpement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -23,7 +23,7 @@
 #include <iosfwd>
 #include <set>
 #include <vector>
-#include "tgba/public.hh"
+#include "tgba/tgba.hh"
 #include "tgbaalgos/scc.hh"
 
 namespace spot