diff --git a/ChangeLog b/ChangeLog
index be43984cd..f5525b140 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,9 @@
 2003-06-26  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments.
+	* src/ltlast/formula.hh: More Doxygen comments.
+	* src/tgba/tgba.hh: Use <tt> in Doxygen comments.
+
 	* doc/mainpage.dox: New file.
 	* doc/Makefile.am (EXTRA_DIST): Add mainpage.dox.
 	* doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox
diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh
index eb8992e22..ea35d049d 100644
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@@ -17,7 +17,9 @@ namespace spot
     public:
       virtual ~formula();
 
+      /// Entry point for vspot::ltl::visitor instances.
       virtual void accept(visitor& v) = 0;
+      /// Entry point for vspot::ltl::const_visitor instances.
       virtual void accept(const_visitor& v) const = 0;
 
       /// \brief clone this formula
@@ -29,7 +31,7 @@ namespace spot
       /// \brief increment reference counter if any
       virtual void ref_();
       /// \brief decrement reference counter if any, return true when
-      /// the instance must be delete (usually when the counter hits 0).
+      /// the instance must be deleted (usually when the counter hits 0).
       virtual bool unref_();
     };
 
diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh
index d5cda6384..be7cc723f 100644
--- a/src/tgba/tgba.hh
+++ b/src/tgba/tgba.hh
@@ -20,12 +20,6 @@ namespace spot
   /// transitions), and a path can be accepted only if it traverse
   /// at least one transition of each set infinitely often.
   ///
-  /// Actually we do not really encode accepting sets but their
-  /// complement: promise sets.  Formulae such as 'a U b' and
-  /// 'F b' make the promise to fulfil 'b' enventually.  A path can
-  /// be accepted if for each promise it traverse infinitely often
-  /// a transition that does not make this promise.
-  ///
   /// Browsing such automaton can be achieved using two functions.
   /// \c get_init_state, and \c succ_iter.  The former returns
   /// the initial state while the latter allows to explore the
@@ -89,11 +83,11 @@ namespace spot
     virtual bdd all_accepting_conditions() const = 0;
 
     /// \brief Return the conjuction of all negated accepting
-    /// variables. 
+    /// variables.
     ///
-    /// For instance if the automaton uses variables \c Acc[a],
-    /// \c Acc[b] and \c Acc[c] to describe accepting sets,
-    /// this function should return \c !Acc[a]\&!Acc[b]\&!Acc[c].
+    /// For instance if the automaton uses variables <tt>Acc[a]</tt>,
+    /// <tt>Acc[b]</tt> and <tt>Acc[c]</tt> to describe accepting sets,
+    /// this function should return <tt>!Acc[a]\&!Acc[b]\&!Acc[c]</tt>.
     ///
     /// This is useful when making products: each operand conditions
     /// set should be augmented with the neg_accepting_conditions() of
diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh
index fca5e44d7..68b21f65a 100644
--- a/src/tgba/tgbabddcoredata.hh
+++ b/src/tgba/tgbabddcoredata.hh
@@ -41,7 +41,7 @@ namespace spot
     /// only concerned by atomic propositions (which label the
     /// transitions) and Next variables (the destination).  Typically,
     /// a transition should bear the variable \c Acc[b] if it doesn't
-    /// check for `b' and have a destination of the form <tt>a U b</tt>, 
+    /// check for `b' and have a destination of the form <tt>a U b</tt>,
     /// or <tt>F b</tt>.
     ///
     /// To summarize, \c accepting_conditions contains three kinds of
@@ -52,7 +52,7 @@ namespace spot
     /// \li "Acc" variables.
     bdd accepting_conditions;
 
-    /// The set of all accepting conditions used by the Automaton.
+    /// \brief The set of all accepting conditions used by the Automaton.
     ///
     /// The goal of the emptiness check is to ensure that
     /// a strongly connected component walks through each
@@ -79,10 +79,10 @@ namespace spot
     /// \brief The (positive) conjunction of all variables which are
     /// not atomic propositions.
     bdd notvar_set;
-    /// The (positive) conjunction of all variables which are not
+    /// \brief The (positive) conjunction of all variables which are not
     /// accepting conditions.
     bdd notacc_set;
-    /// The negative conjunction of all variables which are accepting
+    /// \brief The negative conjunction of all variables which are accepting
     /// conditions.
     bdd negacc_set;