From b89f86edcf44b8142ae0296c3fc2f57f6b3f199e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 25 Aug 2011 12:30:55 +0200
Subject: [PATCH] Mark reduce_tau03() as deprecated.

* src/ltlvisit/contain.hh (reduce_tau03): Mark as deprecated.
* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/ltl2tgba.cc,
src/ltltest/equals.cc: Do not include ltlvisit/contain.hh, since
it's not used.
---
 src/ltltest/equals.cc        |  1 -
 src/ltlvisit/contain.hh      | 11 ++++++++++-
 src/tgbaalgos/ltl2tgba_fm.cc |  1 -
 src/tgbatest/ltl2tgba.cc     |  1 -
 4 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc
index 62ece4878..a0574588b 100644
--- a/src/ltltest/equals.cc
+++ b/src/ltltest/equals.cc
@@ -30,7 +30,6 @@
 #include "ltlvisit/tunabbrev.hh"
 #include "ltlvisit/dump.hh"
 #include "ltlvisit/nenoform.hh"
-#include "ltlvisit/contain.hh"
 #include "ltlast/allnodes.hh"
 #include "ltlvisit/simplify.hh"
 #include "ltlvisit/tostring.hh"
diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh
index ddfe02970..11ad987b3 100644
--- a/src/ltlvisit/contain.hh
+++ b/src/ltlvisit/contain.hh
@@ -1,3 +1,5 @@
+// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+// l'Epita (LRDE).
 // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -95,13 +97,20 @@ namespace spot
     ///  year		= {2003},
     ///  note		= {Reprint of Licentiate's thesis}
     ///}
+    /// \endverbatim
     ///
     /// (The "dagged" cells in the tables are not handled here.)
     ///
     /// If \a stronger is set, additional rules are used to further
     /// reduce some U, R, and X usages.
-    /// \endverbatim
+    ///
+    /// \deprecated Use spot::ltl::ltl_simplifier instead.
+#if __GNUC__
+    formula* reduce_tau03(const formula* f,
+			  bool stronger = true) __attribute__ ((deprecated));
+#else
     formula* reduce_tau03(const formula* f, bool stronger = true);
+#endif
   }
 }
 
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index 6d74ecfe3..b4d94b065 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -36,7 +36,6 @@
 #include <cassert>
 #include <memory>
 #include "ltl2tgba_fm.hh"
-#include "ltlvisit/contain.hh"
 #include "tgba/bddprint.hh"
 
 namespace spot
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index d3bcb0691..4a46dc9a1 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -28,7 +28,6 @@
 #include <fstream>
 #include <string>
 #include <cstdlib>
-#include "ltlvisit/contain.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/apcollect.hh"
 #include "ltlast/allnodes.hh"