diff --git a/m4/gccwarn.m4 b/m4/gccwarn.m4
index 1d78974ad..cf0f324b2 100644
--- a/m4/gccwarn.m4
+++ b/m4/gccwarn.m4
@@ -29,6 +29,7 @@ EOF
    Wpointer-arith \
    Wwrite-strings \
    Wcast-qual \
+   Wdocumentation \
    Werror
   do
     CXXFLAGS="$cf_save_CXXFLAGS $ac_cv_prog_gxx_warn_flags -$cf_opt"
diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh
index c069078b4..11375291e 100644
--- a/src/ltlast/binop.hh
+++ b/src/ltlast/binop.hh
@@ -1,8 +1,9 @@
-// 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 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.
 //
@@ -48,13 +49,13 @@ namespace spot
       enum type { Xor,
 		  Implies,
 		  Equiv,
-		  U, //< until
-		  R, //< release (dual of until)
-		  W, //< weak until
-		  M,  //< strong release (dual of weak until)
-		  EConcat, // Existential Concatenation
-		  EConcatMarked, // Existential Concatenation, Marked
-		  UConcat // Universal Concatenation
+		  U, ///< until
+		  R, ///< release (dual of until)
+		  W, ///< weak until
+		  M, ///< strong release (dual of weak until)
+		  EConcat, ///< Existential Concatenation
+		  EConcatMarked, ///< Existential Concatenation, Marked
+		  UConcat ///< Universal Concatenation
       };
 
       /// \brief Build a unary operator with operation \a op and
diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh
index e4f6019e7..51e90c71d 100644
--- a/src/ltlparse/public.hh
+++ b/src/ltlparse/public.hh
@@ -1,8 +1,9 @@
-// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2010, 2011, 2012, 2013 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),
-// Université Pierre et Marie Curie.
+// Paris 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.
 //
@@ -189,7 +190,7 @@ namespace spot
     /// \param error_list The error list filled by spot::ltl::parse
     ///        or spot::ltl::parse_sere while parsing \a input_string.
     void
-    fix_utf8_locations(const std::string& ltl_string,
+    fix_utf8_locations(const std::string& input_string,
 		       parse_error_list& error_list);
 
     /// @}
diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh
index 75eec9c49..ce26fb25c 100644
--- a/src/ta/taproduct.hh
+++ b/src/ta/taproduct.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2010 Laboratoire de Recherche et Developpement
-// de l Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -35,7 +36,7 @@ namespace spot
   public:
     /// \brief Constructor
     /// \param ta_state The state from the ta automaton.
-    /// \param kripke_state_ The state from Kripke structure.
+    /// \param kripke_state The state from Kripke structure.
     state_ta_product(state* ta_state, state* kripke_state) :
       ta_state_(ta_state), kripke_state_(kripke_state)
     {
diff --git a/src/taalgos/emptinessta.hh b/src/taalgos/emptinessta.hh
index f0bdda165..acf553dc6 100644
--- a/src/taalgos/emptinessta.hh
+++ b/src/taalgos/emptinessta.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2012 Laboratoire de Recherche et Dévelopment de
-// l'Epita (LRDE).
+// Copyright (C) 2008, 2012, 2013 Laboratoire de Recherche et
+// Dévelopment 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),
 // Université Pierre et Marie Curie.
@@ -99,19 +99,19 @@ namespace spot
     ///
     /// Return false if the product automaton accepts no run, otherwise true
     ///
-    /// \param disable_second_pass: is used to disable the second pass when
+    /// \param disable_second_pass is used to disable the second pass when
     /// when it is not necessary, for example when all the livelock-accepting
     /// states of the TA automaton have no successors, we call this kind of
     /// TA as STA (Single-pass Testing Automata)
     /// (see spot::tgba2ta::add_artificial_livelock_accepting_state() for an
     /// automatic transformation of any TA automaton into STA automaton
     ///
-    /// \param disable_heuristic_for_livelock_detection: disable the heuristic
+    /// \param disable_heuristic_for_livelock_detection disable the heuristic
     /// used in the first pass to detect livelock-accepting runs,
     /// this heuristic is described in the paper cited above
     virtual bool
     check(bool disable_second_pass = false,
-        bool disable_heuristic_for_livelock_detection = false);
+	  bool disable_heuristic_for_livelock_detection = false);
 
     /// \brief Check whether the product automaton contains
     /// a livelock-accepting run
diff --git a/src/taalgos/reachiter.hh b/src/taalgos/reachiter.hh
index d7913b516..4e266b2b8 100644
--- a/src/taalgos/reachiter.hh
+++ b/src/taalgos/reachiter.hh
@@ -1,6 +1,6 @@
-// Copyright (C) 2010 Laboratoire de Recherche et Developpement
-// de l Epita (LRDE).
-//
+// -*- coding: utf-8 -*-
+// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -74,21 +74,14 @@ namespace spot
     ///
     /// \param s The current state.
     /// \param n A unique number assigned to \a s.
-    /// \param si The spot::ta_succ_iterator for \a s.
     virtual void
     process_state(const state* s, int n);
     /// Called by run() to process a transition.
     ///
-    /// \param in_s The source state
     /// \param in The source state number.
-    /// \param out_s The destination state
     /// \param out The destination state number.
     /// \param si The spot::tgba_succ_iterator positionned on the current
     ///             transition.
-    ///
-    /// The in_s and out_s states are owned by the
-    /// spot::ta_reachable_iterator instance and destroyed when the
-    /// instance is destroyed.
     virtual void
     process_link(int in, int out, const ta_succ_iterator* si);
 
diff --git a/src/tgba/state.hh b/src/tgba/state.hh
index c6af2dfac..528894dd9 100644
--- a/src/tgba/state.hh
+++ b/src/tgba/state.hh
@@ -1,7 +1,8 @@
-// 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).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
-// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
+// (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.
@@ -78,10 +79,10 @@ namespace spot
     /// Methods from the tgba or tgba_succ_iterator always return a
     /// new state that you should deallocate with this function.
     /// Before Spot 0.7, you had to "delete" your state directly.
-    /// Starting with Spot 0.7, you update your code to this function
-    /// instead (which simply calls "delete").  In a future version,
-    /// some subclasses will redefine destroy() to allow better memory
-    /// management (e.g. no memory allocation for explicit automata).
+    /// Starting with Spot 0.7, you should update your code to use
+    /// this function instead. destroy() usually call delete, except
+    /// in subclasses that destroy() to allow better memory management
+    /// (e.g., no memory allocation for explicit automata).
     virtual void destroy() const
     {
       delete this;
@@ -90,7 +91,7 @@ namespace spot
   protected:
     /// \brief Destructor.
     ///
-    /// \deprecated Client code should now call
+    /// Note that client code should call
     /// <code>s->destroy();</code> instead of <code>delete s;</code>.
     virtual ~state()
     {
diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc
index 812bff971..d2eb770b2 100644
--- a/src/tgba/tgbasafracomplement.cc
+++ b/src/tgba/tgbasafracomplement.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -191,7 +191,7 @@ namespace spot
 
     /// \brief Compare two safra trees.
     ///
-    /// \param other
+    /// \param other the tree to compare too.
     ///
     /// \return 0 if the trees are the same. Otherwise
     /// a signed value.
@@ -520,7 +520,7 @@ namespace spot
     ///
     /// \param bitset a bitset of size \c this->get_nb_acceptance_pairs()
     /// filled with FALSE bits.
-    /// \return bitset[i] will be true if this state-tree is included in L_i
+    /// On return bitset[i] will be set if this state-tree is included in L_i.
     void
     safra_tree::getL(bitset_t& bitset) const
     {
@@ -538,7 +538,7 @@ namespace spot
     ///
     /// \param bitset a bitset of size \c this->get_nb_acceptance_pairs()
     /// filled with TRUE bits.
-    /// \return bitset[i] will be true if this state-tree is included in U_i
+    /// On return bitset[i] will be set if this state-tree is included in U_i.
     void
     safra_tree::getU(bitset_t& bitset) const
     {
@@ -1202,7 +1202,7 @@ namespace spot
   ///   publisher     = {Springer-Verlag}
   /// }
   ///
-  /// @param local_state
+  /// @param local_state the state from which we want to compute the successors.
   ///
   tgba_succ_iterator*
   tgba_safra_complement::succ_iter(const state* local_state,
diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh
index 155095863..68306245f 100644
--- a/src/tgbaalgos/ltl2tgba_fm.hh
+++ b/src/tgbaalgos/ltl2tgba_fm.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
+// Copyright (C) 2010, 2011, 2012, 2013 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),
@@ -97,11 +97,12 @@ namespace spot
   /// formula are observable events, and \c unobs can be filled with
   /// additional unobservable events.
   ///
-  /// \param simpl If this parameter is set, the LTL formulae representing
-  /// each state of the automaton will be simplified
+  /// \param simplifier If this parameter is set, the LTL formulae
+  /// representing each state of the automaton will be simplified
   /// before computing the successor.  \a simpl should be configured
-  /// for the type of reduction you want, see spot::ltl::ltl_simplifier.
-  /// This idea is taken from the following paper.
+  /// for the type of reduction you want, see
+  /// spot::ltl::ltl_simplifier.  This idea is taken from the
+  /// following paper.
   /// \verbatim
   /// @InProceedings{	  thirioux.02.fmics,
   ///   author	  = {Xavier Thirioux},