From 20bdf49a70082ce4a6f948912f4d35c573a96060 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 25 May 2004 12:55:48 +0000
Subject: [PATCH] * src/ltlvisit/reducform.hh: Update Doxygen comments for
 previous change.

---
 ChangeLog                 |  3 +++
 src/ltlvisit/reducform.hh | 20 +++++++++++---------
 2 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 07f841064..12ab752f7 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,8 @@
 2004-05-25  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/ltlvisit/reducform.hh: Update Doxygen comments for
+	previous change.
+
 	* src/ltlvisit/reducform.hh (option): Rename as ...
 	(reduce_options): ... this, and use it as a bit field so
 	option can be combined easily.
diff --git a/src/ltlvisit/reducform.hh b/src/ltlvisit/reducform.hh
index 84dcfd1f4..dc25d9bac 100644
--- a/src/ltlvisit/reducform.hh
+++ b/src/ltlvisit/reducform.hh
@@ -30,25 +30,27 @@ namespace spot
   namespace ltl
   {
 
+    /// Options for spot::ltl::reduce.
     enum reduce_options
       {
+	/// No reduction.
 	Reduce_None = 0,
+	/// Basic reductions.
 	Reduce_Basics = 1,
+	/// Somenzi & Bloem syntactic implication.
 	Reduce_Syntactic_Implications = 2,
+	/// Etessami & Holzmann eventuality and universality reductions.
 	Reduce_Eventuality_And_Universality = 4,
+	/// All reductions.
 	Reduce_All = -1U
       };
 
-    /// \brief Reduce a formula \a f using Basic rewriting, implies
-    /// relation, and class of eventuality and univerality formula.
+    /// \brief Reduce a formula \a f.
     ///
-    /// Put the formula in negative normal form with
-    /// spot::ltl::negative_normal_form and then reduce it according
-    /// to options:
-    /// Base for spot::ltl::Basic_reduce_form,
-    /// Inf for spot::ltl::reduce_inf_form,
-    /// EventualUniversal for spot::ltl::reduce_eventuality_universality_form,
-    /// BRI for spot::ltl::reduce_form.
+    /// \param f the formula to reduce
+    /// \param opt a conjonction of spot::ltl::reduce_options specifying
+    //             which optimizations to apply.
+    /// \return the reduced formula
     formula* reduce(const formula* f, int opt = Reduce_All);
 
     /// Implement basic rewriting.