diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index ff8b9bf56..8a466b7b6 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -32,7 +32,7 @@
 
 #include "tgbaalgos/dotty.hh"
 #include "tgbaalgos/lbtt.hh"
-#include "tgbaalgos/hoaf.hh"
+#include "tgbaalgos/hoa.hh"
 #include "tgbaalgos/neverclaim.hh"
 #include "tgbaalgos/save.hh"
 #include "tgbaalgos/stats.hh"
@@ -127,7 +127,7 @@ const struct argp_child children[] =
 enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot;
 bool utf8 = false;
 const char* stats = "";
-const char* hoaf_opt = 0;
+const char* hoa_opt = 0;
 spot::option_map extra_options;
 
 static int
@@ -147,7 +147,7 @@ parse_opt(int key, char* arg, struct argp_state*)
       break;
     case 'H':
       format = Hoa;
-      hoaf_opt = arg;
+      hoa_opt = arg;
       break;
     case 'M':
       type = spot::postprocessor::Monitor;
@@ -315,7 +315,7 @@ namespace
 	  spot::lbtt_reachable(std::cout, aut, false);
 	  break;
 	case Hoa:
-	  spot::hoaf_reachable(std::cout, aut, hoaf_opt) << '\n';
+	  spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
 	  break;
 	case Spot:
 	  spot::tgba_save_reachable(std::cout, aut);
diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc
index 27e0e7832..c84ab8bc0 100644
--- a/src/bin/dstar2tgba.cc
+++ b/src/bin/dstar2tgba.cc
@@ -32,7 +32,7 @@
 
 #include "tgbaalgos/dotty.hh"
 #include "tgbaalgos/lbtt.hh"
-#include "tgbaalgos/hoaf.hh"
+#include "tgbaalgos/hoa.hh"
 #include "tgbaalgos/neverclaim.hh"
 #include "tgbaalgos/save.hh"
 #include "tgbaalgos/stats.hh"
@@ -128,7 +128,7 @@ const struct argp_child children[] =
 enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot;
 bool utf8 = false;
 const char* stats = "";
-const char* hoaf_opt = 0;
+const char* hoa_opt = 0;
 spot::option_map extra_options;
 
 static int
@@ -148,7 +148,7 @@ parse_opt(int key, char* arg, struct argp_state*)
       break;
     case 'H':
       format = Hoa;
-      hoaf_opt = arg;
+      hoa_opt = arg;
       break;
     case 'M':
       type = spot::postprocessor::Monitor;
@@ -324,7 +324,7 @@ namespace
 	  spot::lbtt_reachable(std::cout, aut, false);
 	  break;
 	case Hoa:
-	  spot::hoaf_reachable(std::cout, aut, hoaf_opt) << '\n';
+	  spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
 	  break;
 	case Spot:
 	  spot::tgba_save_reachable(std::cout, aut);
diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc
index 4b3d9a6c5..9989187d6 100644
--- a/src/bin/ltl2tgba.cc
+++ b/src/bin/ltl2tgba.cc
@@ -38,7 +38,7 @@
 #include "tgbaalgos/lbtt.hh"
 #include "tgbaalgos/neverclaim.hh"
 #include "tgbaalgos/save.hh"
-#include "tgbaalgos/hoaf.hh"
+#include "tgbaalgos/hoa.hh"
 #include "tgbaalgos/stats.hh"
 #include "tgbaalgos/translate.hh"
 #include "tgba/bddprint.hh"
@@ -73,7 +73,7 @@ static const argp_option options[] =
     { "csv-escape", OPT_CSV, 0, 0, "quote formula output by %f in --format "
       "for use in CSV file", 0 },
     { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 },
-    { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL,
+    { "hoa", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL,
       "Output the automaton in HOA format.  Add letters to select "
       "(s) state-based acceptance, (t) transition-based acceptance, "
       "(m) mixed acceptance, (l) single-line output", 0 },
@@ -126,7 +126,7 @@ const struct argp_child children[] =
 enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot;
 bool utf8 = false;
 const char* stats = "";
-const char* hoaf_opt = 0;
+const char* hoa_opt = 0;
 spot::option_map extra_options;
 
 static int
@@ -144,7 +144,7 @@ parse_opt(int key, char* arg, struct argp_state*)
       break;
     case 'H':
       format = Hoa;
-      hoaf_opt = arg;
+      hoa_opt = arg;
       break;
     case 'M':
       type = spot::postprocessor::Monitor;
@@ -254,7 +254,7 @@ namespace
 	  spot::lbtt_reachable(std::cout, aut, false);
 	  break;
 	case Hoa:
-	  spot::hoaf_reachable(std::cout, aut, hoaf_opt, f) << '\n';
+	  spot::hoa_reachable(std::cout, aut, hoa_opt, f) << '\n';
 	  break;
 	case Spot:
 	  spot::tgba_save_reachable(std::cout, aut);
diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am
index 314f193eb..89818cc20 100644
--- a/src/tgbaalgos/Makefile.am
+++ b/src/tgbaalgos/Makefile.am
@@ -43,7 +43,7 @@ tgbaalgos_HEADERS = \
   emptiness.hh \
   emptiness_stats.hh \
   gv04.hh \
-  hoaf.hh \
+  hoa.hh \
   isdet.hh \
   isweakscc.hh \
   lbtt.hh \
@@ -93,7 +93,7 @@ libtgbaalgos_la_SOURCES = \
   dupexp.cc \
   emptiness.cc \
   gv04.cc \
-  hoaf.cc \
+  hoa.cc \
   isdet.cc \
   isweakscc.cc \
   lbtt.cc \
diff --git a/src/tgbaalgos/hoaf.cc b/src/tgbaalgos/hoa.cc
similarity index 87%
rename from src/tgbaalgos/hoaf.cc
rename to src/tgbaalgos/hoa.cc
index 33bc5f28d..9ed19834a 100644
--- a/src/tgbaalgos/hoaf.cc
+++ b/src/tgbaalgos/hoa.cc
@@ -24,7 +24,7 @@
 #include <sstream>
 #include <map>
 #include "tgba/tgba.hh"
-#include "hoaf.hh"
+#include "hoa.hh"
 #include "reachiter.hh"
 #include "misc/escape.hh"
 #include "misc/bddlt.hh"
@@ -226,20 +226,20 @@ namespace spot
 
 
   std::ostream&
-  hoaf_reachable(std::ostream& os,
-		 const const_tgba_ptr& aut,
-		 const ltl::formula* f,
-		 hoaf_acceptance acceptance,
-		 hoaf_alias alias,
-		 bool newline)
+  hoa_reachable(std::ostream& os,
+		const const_tgba_ptr& aut,
+		const ltl::formula* f,
+		hoa_acceptance acceptance,
+		hoa_alias alias,
+		bool newline)
   {
     (void) alias;
 
     metadata md(aut);
 
-    if (acceptance == Hoaf_Acceptance_States
+    if (acceptance == Hoa_Acceptance_States
 	&& !md.state_acc)
-      acceptance = Hoaf_Acceptance_Transitions;
+      acceptance = Hoa_Acceptance_Transitions;
 
     unsigned num_states = md.nm.size();
 
@@ -281,9 +281,9 @@ namespace spot
       }
     os << nl;
     os << "properties: trans-labels explicit-labels";
-    if (acceptance == Hoaf_Acceptance_States)
+    if (acceptance == Hoa_Acceptance_States)
       os << " state-acc";
-    else if (acceptance == Hoaf_Acceptance_Transitions)
+    else if (acceptance == Hoa_Acceptance_Transitions)
       os << " trans-acc";
     if (md.is_complete)
       os << " complete";
@@ -293,16 +293,16 @@ namespace spot
     os << "--BODY--" << nl;
     for (unsigned i = 0; i < num_states; ++i)
       {
-	hoaf_acceptance this_acc = acceptance;
-	if (this_acc == Hoaf_Acceptance_Mixed)
+	hoa_acceptance this_acc = acceptance;
+	if (this_acc == Hoa_Acceptance_Mixed)
 	  this_acc = (md.common_acc[i] ?
-		      Hoaf_Acceptance_States : Hoaf_Acceptance_Transitions);
+		      Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
 
 	tgba_succ_iterator* j = aut->succ_iter(md.nm[i]);
 	j->first();
 
 	os << "State: " << i;
-	if (this_acc == Hoaf_Acceptance_States && !j->done())
+	if (this_acc == Hoa_Acceptance_States && !j->done())
 	  md.emit_acc(os, aut, j->current_acceptance_conditions());
 	os << nl;
 
@@ -310,7 +310,7 @@ namespace spot
 	  {
 	    const state* dst = j->current_state();
 	    os << '[' << md.sup[j->current_condition()] << "] " << md.sm[dst];
-	    if (this_acc == Hoaf_Acceptance_Transitions)
+	    if (this_acc == Hoa_Acceptance_Transitions)
 	      md.emit_acc(os, aut, j->current_acceptance_conditions());
 	    os << nl;
 	    dst->destroy();
@@ -324,14 +324,14 @@ namespace spot
   }
 
   std::ostream&
-  hoaf_reachable(std::ostream& os,
-		 const const_tgba_ptr& aut,
-		 const char* opt,
-		 const ltl::formula* f)
+  hoa_reachable(std::ostream& os,
+		const const_tgba_ptr& aut,
+		const char* opt,
+		const ltl::formula* f)
   {
     bool newline = true;
-    hoaf_acceptance acceptance = Hoaf_Acceptance_States;
-    hoaf_alias alias = Hoaf_Alias_None;
+    hoa_acceptance acceptance = Hoa_Acceptance_States;
+    hoa_alias alias = Hoa_Alias_None;
 
     if (opt)
       while (*opt)
@@ -342,17 +342,17 @@ namespace spot
 	      newline = false;
 	      break;
 	    case 'm':
-	      acceptance = Hoaf_Acceptance_Mixed;
+	      acceptance = Hoa_Acceptance_Mixed;
 	      break;
 	    case 's':
-	      acceptance = Hoaf_Acceptance_States;
+	      acceptance = Hoa_Acceptance_States;
 	      break;
 	    case 't':
-	      acceptance = Hoaf_Acceptance_Transitions;
+	      acceptance = Hoa_Acceptance_Transitions;
 	      break;
 	    }
 	}
-    return hoaf_reachable(os, aut, f, acceptance, alias, newline);
+    return hoa_reachable(os, aut, f, acceptance, alias, newline);
   }
 
 }
diff --git a/src/tgbaalgos/hoaf.hh b/src/tgbaalgos/hoa.hh
similarity index 68%
rename from src/tgbaalgos/hoaf.hh
rename to src/tgbaalgos/hoa.hh
index 5f405c088..a1b1829b7 100644
--- a/src/tgbaalgos/hoaf.hh
+++ b/src/tgbaalgos/hoa.hh
@@ -17,8 +17,8 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
-#ifndef SPOT_TGBAALGOS_HOAF_HH
-# define SPOT_TGBAALGOS_HOAF_HH
+#ifndef SPOT_TGBAALGOS_HOA_HH
+# define SPOT_TGBAALGOS_HOA_HH
 
 #include <iosfwd>
 #include "ltlast/formula.hh"
@@ -26,15 +26,15 @@
 
 namespace spot
 {
-  enum hoaf_alias { Hoaf_Alias_None, Hoaf_Alias_Ap, Hoaf_Alias_Cond };
-  enum hoaf_acceptance
+  enum hoa_alias { Hoa_Alias_None, Hoa_Alias_Ap, Hoa_Alias_Cond };
+  enum hoa_acceptance
     {
-      Hoaf_Acceptance_States,	/// state-based acceptance if
+      Hoa_Acceptance_States,	/// state-based acceptance if
 				/// (globally) possible
 				/// transition-based acceptance
 				/// otherwise.
-      Hoaf_Acceptance_Transitions, /// transition-based acceptance globally
-      Hoaf_Acceptance_Mixed  /// mix state-based and transition-based
+      Hoa_Acceptance_Transitions, /// transition-based acceptance globally
+      Hoa_Acceptance_Mixed    /// mix state-based and transition-based
     };
 
   /// \ingroup tgba_io
@@ -49,18 +49,18 @@ namespace spot
   /// \param alias Whether aliases should be used in output.
   /// \param newlines Whether to use newlines in output.
   SPOT_API std::ostream&
-  hoaf_reachable(std::ostream& os,
-		 const const_tgba_ptr& g,
-		 const ltl::formula* f = 0,
-		 hoaf_acceptance acceptance = Hoaf_Acceptance_States,
-		 hoaf_alias alias = Hoaf_Alias_None,
-		 bool newlines = true);
+  hoa_reachable(std::ostream& os,
+		const const_tgba_ptr& g,
+		const ltl::formula* f = 0,
+		hoa_acceptance acceptance = Hoa_Acceptance_States,
+		hoa_alias alias = Hoa_Alias_None,
+		bool newlines = true);
 
   SPOT_API std::ostream&
-  hoaf_reachable(std::ostream& os,
-		 const const_tgba_ptr& g,
-		 const char* opt,
-		 const ltl::formula* f = 0);
+  hoa_reachable(std::ostream& os,
+		const const_tgba_ptr& g,
+		const char* opt,
+		const ltl::formula* f = 0);
 }
 
-#endif // SPOT_TGBAALGOS_HOAF_HH
+#endif // SPOT_TGBAALGOS_HOA_HH
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 4a8b1a7de..a600c45f5 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -36,7 +36,7 @@
 #include "tgbaalgos/save.hh"
 #include "tgbaalgos/dotty.hh"
 #include "tgbaalgos/lbtt.hh"
-#include "tgbaalgos/hoaf.hh"
+#include "tgbaalgos/hoa.hh"
 #include "tgbaalgos/degen.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgbaalgos/reducerun.hh"
@@ -385,7 +385,7 @@ checked_main(int argc, char** argv)
   bool opt_closure = false;
   bool opt_stutterize = false;
   bool spin_comments = false;
-  const char* hoaf_opt = 0;
+  const char* hoa_opt = 0;
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* unobservables = 0;
   spot::tgba_ptr system_aut = 0;
@@ -554,7 +554,7 @@ checked_main(int argc, char** argv)
       else if (!strncmp(argv[formula_index], "-H", 2))
 	{
 	  output = 17;
-	  hoaf_opt = argv[formula_index] + 2;
+	  hoa_opt = argv[formula_index] + 2;
 	}
       else if (!strcmp(argv[formula_index], "-k"))
 	{
@@ -1718,7 +1718,7 @@ checked_main(int argc, char** argv)
 	      }
 	    case 17:
 	      {
-		hoaf_reachable(std::cout, a, hoaf_opt, f) << '\n';
+		hoa_reachable(std::cout, a, hoa_opt, f) << '\n';
 		break;
 	      }
 	    default: