diff --git a/ChangeLog b/ChangeLog
index fce3c828b..cb89d2c43 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,7 @@
 2004-11-02  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/ltlvisit/reduce.hh (is_eventual, is_universal): More doc.
+
 	* src/tgbaalgos/projrun.hh, src/tgbaalgos/projrun.cc: New files.
 	* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
 	libtgbaalgos_la_SOURCES): Add them.
diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh
index 301e65a20..365a10f22 100644
--- a/src/ltlvisit/reduce.hh
+++ b/src/ltlvisit/reduce.hh
@@ -53,9 +53,9 @@ namespace spot
     /// \return the reduced formula
     formula* reduce(const formula* f, int opt = Reduce_All);
 
-    /// \brief Check whether a formula is eventual.
+    /// \brief Check whether a formula is a pure eventuality.
     ///
-    /// This comes from
+    /// Pure eventuality formulae are defined in
     /// \verbatim
     /// @InProceedings{	  etessami.00.concur,
     /// author  	= {Kousha Etessami and Gerard J. Holzmann},
@@ -70,12 +70,31 @@ namespace spot
     /// publisher	= {Springer-Verlag}
     /// }
     /// \endverbatim
-    /// FIXME: Describe what eventual formulae are.
+    ///
+    /// A word that satisfies a pure eventuality can be prefixed by
+    /// anything and still satisfies the formula.
     bool is_eventual(const formula* f);
 
-    /// \brief Check whether a formula is universal.
+    /// \brief Check whether a formula is purely universal.
     ///
-    /// FIXME: Describe what universal formulae are.  Cite paper.
+    /// Purely universal formulae are defined in
+    /// \verbatim
+    /// @InProceedings{	  etessami.00.concur,
+    /// author  	= {Kousha Etessami and Gerard J. Holzmann},
+    /// title		= {Optimizing {B\"u}chi Automata},
+    /// booktitle	= {Proceedings of the 11th International Conference on
+    /// 		  Concurrency Theory (Concur'2000)},
+    /// pages		= {153--167},
+    /// year		= {2000},
+    /// editor  	= {C. Palamidessi},
+    /// volume  	= {1877},
+    /// series  	= {Lecture Notes in Computer Science},
+    /// publisher	= {Springer-Verlag}
+    /// }
+    /// \endverbatim
+    ///
+    /// Any (non-empty) suffix of a word that satisfies if purely
+    /// universal formula also satisfies the formula.
     bool is_universal(const formula* f);
   }
 }