diff --git a/ChangeLog b/ChangeLog
index 96b628d34..adfb27e1b 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,12 @@
-2003-04-16  Alexandre DURET-LUTZ  <aduret@circe.lip6.fr>
+2003-04-16  Alexandre DURET-LUTZ  <aduret@src.lip6.fr>
 
+	* src/ltlast/formulae.hh: Rename as ...
+	* src/ltlast/formula.hh: ... this.
+	* src/ltlast/Makefile.am (libltlast_a_SOURCES): Adjust.
+	* src/ltlast/formula.hh (formulae): Rename as ...
+	(formula): ... this.
+	Adjust all uses.
+	
 	* src/ltlparse/public.hh (format_parse_errors): New function.
 	* src/ltlparse/fmterror.cc: New file.
 	* src/ltlparse/Makefile.am (libltlparse_a_SOURCES): Add fmterror.cc.
diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am
index af0fc8692..d9a9de821 100644
--- a/src/ltlast/Makefile.am
+++ b/src/ltlast/Makefile.am
@@ -10,7 +10,7 @@ libltlast_a_SOURCES = \
   binop.hh \
   constant.cc \
   constant.hh \
-  formulae.hh \
+  formula.hh \
   multop.cc \
   multop.hh \
   predecl.hh \
diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh
index 35d607934..a8fefc511 100644
--- a/src/ltlast/atomic_prop.hh
+++ b/src/ltlast/atomic_prop.hh
@@ -2,14 +2,14 @@
 # define SPOT_LTLAST_ATOMIC_PROP_HH
 
 #include <string>
-#include "formulae.hh"
+#include "formula.hh"
 
 namespace spot
 {
   namespace ltl
   {
     
-    class atomic_prop : public formulae
+    class atomic_prop : public formula
     {
     public:
       atomic_prop(std::string name);
diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index d797f41d1..7aac72fbb 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -6,7 +6,7 @@ namespace spot
 {
   namespace ltl
   {    
-    binop::binop(type op, formulae* first, formulae* second)
+    binop::binop(type op, formula* first, formula* second)
       : op_(op), first_(first), second_(second)
     {
     }
@@ -27,25 +27,25 @@ namespace spot
       v.visit(this);
     }
 
-    const formulae*
+    const formula*
     binop::first() const
     {
       return first_;
     }
 
-    formulae*
+    formula*
     binop::first()
     {
       return first_;
     }
 
-    const formulae*
+    const formula*
     binop::second() const
     {
       return second_;
     }
 
-    formulae* 
+    formula* 
     binop::second()
     {
       return second_;
diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh
index b755e3f9a..e7c10ba7e 100644
--- a/src/ltlast/binop.hh
+++ b/src/ltlast/binop.hh
@@ -1,38 +1,38 @@
 #ifndef SPOT_LTLAST_BINOP_HH
 # define SPOT_LTLAST_BINOP_HH
 
-#include "formulae.hh"
+#include "formula.hh"
 
 namespace spot
 {
   namespace ltl
   {
     
-    class binop : public formulae
+    class binop : public formula
     {
     public:
       // And and Or are not here.  Because they
       // are often nested we represent them as multops.
       enum type { Xor, Implies, Equiv, U, R };
 
-      binop(type op, formulae* first, formulae* second);
+      binop(type op, formula* first, formula* second);
       virtual ~binop();
 
       virtual void accept(visitor& v);
       virtual void accept(const_visitor& v) const;
 
-      const formulae* first() const;
-      formulae* first();
-      const formulae* second() const;
-      formulae* second();
+      const formula* first() const;
+      formula* first();
+      const formula* second() const;
+      formula* second();
 
       type op() const;
       const char* op_name() const;
 
     private:
       type op_;
-      formulae* first_;
-      formulae* second_;
+      formula* first_;
+      formula* second_;
     };
 
   }
diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh
index 5f8e2dc3f..dcd4b3b58 100644
--- a/src/ltlast/constant.hh
+++ b/src/ltlast/constant.hh
@@ -1,14 +1,14 @@
 #ifndef SPOT_LTLAST_CONSTANT_HH
 # define SPOT_LTLAST_CONSTANT_HH
 
-#include "formulae.hh"
+#include "formula.hh"
 
 namespace spot
 {
   namespace ltl
   {
     
-    class constant : public formulae
+    class constant : public formula
     {
     public:
       enum type { False, True };
@@ -19,8 +19,8 @@ namespace spot
       virtual void accept(visitor& v);
       virtual void accept(const_visitor& v) const;
 
-      const formulae* child() const;
-      formulae* child();
+      const formula* child() const;
+      formula* child();
 
       type val() const;
       const char* val_name() const;
diff --git a/src/ltlast/formulae.hh b/src/ltlast/formula.hh
similarity index 93%
rename from src/ltlast/formulae.hh
rename to src/ltlast/formula.hh
index 03378f8b4..f46e19eb0 100644
--- a/src/ltlast/formulae.hh
+++ b/src/ltlast/formula.hh
@@ -8,7 +8,7 @@ namespace spot
   namespace ltl 
   {
 
-    class formulae 
+    class formula 
     {
     public:
       virtual void accept(visitor& v) = 0;
diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc
index fc37772b7..ce7b034b3 100644
--- a/src/ltlast/multop.cc
+++ b/src/ltlast/multop.cc
@@ -7,7 +7,7 @@ namespace spot
 {
   namespace ltl
   {    
-    multop::multop(type op, formulae* first, formulae* second)
+    multop::multop(type op, formula* first, formula* second)
       : op_(op)
     {
       children_.reserve(2);
@@ -16,9 +16,9 @@ namespace spot
     }
     
     void
-    multop::add(formulae* f)
+    multop::add(formula* f)
     {
-      // If the formulae we add is itself a multop for the same operator,
+      // If the formula we add is itself a multop for the same operator,
       // merge its children with ours.
       multop* p = dynamic_cast<multop*>(f);
       if (p && p->op() == op())
@@ -26,7 +26,7 @@ namespace spot
 	  unsigned ps = p->size();
 	  for (unsigned i = 0; i < ps; ++i)
 	    children_.push_back(p->nth(i));
-	  // that sub-formulae is now useless 
+	  // that sub-formula is now useless 
 	  delete f;
 	}
       else
@@ -57,13 +57,13 @@ namespace spot
       return children_.size();
     }
 
-    const formulae*
+    const formula*
     multop::nth(unsigned n) const
     {
       return children_[n];
     }
 
-    formulae* 
+    formula* 
     multop::nth(unsigned n)
     {
       return children_[n];
diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh
index 18cee2250..40722e0e4 100644
--- a/src/ltlast/multop.hh
+++ b/src/ltlast/multop.hh
@@ -2,22 +2,22 @@
 # define SPOT_LTLAST_MULTOP_HH
 
 #include <vector>
-#include "formulae.hh"
+#include "formula.hh"
 
 namespace spot
 {
   namespace ltl
   {
     
-    class multop : public formulae
+    class multop : public formula
     {
     public:
       enum type { Or, And };
 
       // A multop has at least two arguments.
-      multop(type op, formulae* first, formulae* second);
+      multop(type op, formula* first, formula* second);
       // More argument can be added.
-      void add(formulae* f);
+      void add(formula* f);
       
       virtual ~multop();
 
@@ -25,15 +25,15 @@ namespace spot
       virtual void accept(const_visitor& v) const;
 
       unsigned size() const;
-      const formulae* nth(unsigned n) const;
-      formulae* nth(unsigned n);
+      const formula* nth(unsigned n) const;
+      formula* nth(unsigned n);
 
       type op() const;
       const char* op_name() const;
 
     private:
       type op_;
-      std::vector<formulae*> children_;
+      std::vector<formula*> children_;
     };
 
   }
diff --git a/src/ltlast/predecl.hh b/src/ltlast/predecl.hh
index 8dfb679a6..6bb204f1a 100644
--- a/src/ltlast/predecl.hh
+++ b/src/ltlast/predecl.hh
@@ -10,7 +10,7 @@ namespace spot {
     struct unop;
     struct constant;
     struct binop;
-    struct formulae;
+    struct formula;
     struct multop;
   }
 }
diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc
index 02eb664f5..f4f205b1e 100644
--- a/src/ltlast/unop.cc
+++ b/src/ltlast/unop.cc
@@ -6,7 +6,7 @@ namespace spot
 {
   namespace ltl
   {    
-    unop::unop(type op, formulae* child)
+    unop::unop(type op, formula* child)
       : op_(op), child_(child)
     {
     }
@@ -27,13 +27,13 @@ namespace spot
       v.visit(this);
     }
 
-    const formulae*
+    const formula*
     unop::child() const
     {
       return child_;
     }
 
-    formulae*
+    formula*
     unop::child()
     {
       return child_;
diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh
index 38e28e745..b6ce7831d 100644
--- a/src/ltlast/unop.hh
+++ b/src/ltlast/unop.hh
@@ -1,33 +1,33 @@
 #ifndef SPOT_LTLAST_UNOP_HH
 # define SPOT_LTLAST_UNOP_HH
 
-#include "formulae.hh"
+#include "formula.hh"
 
 namespace spot
 {
   namespace ltl
   {
     
-    class unop : public formulae
+    class unop : public formula
     {
     public:
       enum type { Not, X, F, G };
 
-      unop(type op, formulae* child);
+      unop(type op, formula* child);
       virtual ~unop();
 
       virtual void accept(visitor& v);
       virtual void accept(const_visitor& v) const;
 
-      const formulae* child() const;
-      formulae* child();
+      const formula* child() const;
+      formula* child();
 
       type op() const;
       const char* op_name() const;
 
     private:
       type op_;
-      formulae* child_;
+      formula* child_;
     };
 
   }
diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index 0f17b8a02..16e76a566 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/src/ltlparse/ltlparse.yy
@@ -3,7 +3,7 @@
 #include "public.hh"
 #include "ltlast/allnodes.hh"
 
-extern spot::ltl::formulae* result;
+extern spot::ltl::formula* result;
 
 %}
 
@@ -13,7 +13,7 @@ extern spot::ltl::formulae* result;
 {
   int token;
   std::string* str;
-  spot::ltl::formulae* ltl;
+  spot::ltl::formula* ltl;
 }
 
 %{
@@ -58,10 +58,10 @@ namespace spot
 %token CONST_FALSE
 %token END_OF_INPUT
 
-%type <ltl> result ltl_formulae subformulae
+%type <ltl> result ltl_formula subformula
 
 %%
-result:       ltl_formulae END_OF_INPUT
+result:       ltl_formula END_OF_INPUT
               { result = $$ = $1; 
 		YYACCEPT;
 	      }
@@ -82,57 +82,57 @@ many_errors_diagnosed : many_errors
               { error_list->push_back(parse_error(@1, 
 				     "unexpected input ignored")); }
 
-ltl_formulae: subformulae
+ltl_formula: subformula
               { $$ = $1; }
-	    | many_errors_diagnosed subformulae
+	    | many_errors_diagnosed subformula
               { $$ = $2; }
-	    | ltl_formulae many_errors_diagnosed
+	    | ltl_formula many_errors_diagnosed
               { $$ = $1; }
 
 many_errors: error
 	    | many_errors error
 
-subformulae: ATOMIC_PROP
+subformula: ATOMIC_PROP
 	      { $$ = new atomic_prop(*$1); delete $1; }
 	    | CONST_TRUE
               { $$ = new constant(constant::True); }
 	    | CONST_FALSE
               { $$ = new constant(constant::False); }
-	    | PAR_OPEN subformulae PAR_CLOSE
+	    | PAR_OPEN subformula PAR_CLOSE
 	      { $$ = $2; }
 	    | PAR_OPEN error PAR_CLOSE
               { error_list->push_back(parse_error(@$, 
                  "treating this parenthetical block as false")); 
 	        $$ = new constant(constant::False);
 	      }
-	    | PAR_OPEN subformulae many_errors PAR_CLOSE
+	    | PAR_OPEN subformula many_errors PAR_CLOSE
               { error_list->push_back(parse_error(@3, 
 				      "unexpected input ignored")); 
 	        $$ = $2;
 	      }
-	    | OP_NOT subformulae
+	    | OP_NOT subformula
 	      { $$ = new unop(unop::Not, $2); }
-            | subformulae OP_AND subformulae
+            | subformula OP_AND subformula
 	      { $$ = new multop(multop::And, $1, $3); }
-	    | subformulae OP_OR subformulae
+	    | subformula OP_OR subformula
 	      { $$ = new multop(multop::Or, $1, $3); }
-	    | subformulae OP_XOR subformulae
+	    | subformula OP_XOR subformula
 	      { $$ = new binop(binop::Xor, $1, $3); }
-	    | subformulae OP_IMPLIES subformulae
+	    | subformula OP_IMPLIES subformula
 	      { $$ = new binop(binop::Implies, $1, $3); }
-            | subformulae OP_EQUIV subformulae
+            | subformula OP_EQUIV subformula
 	      { $$ = new binop(binop::Equiv, $1, $3); }
-            | subformulae OP_U subformulae
+            | subformula OP_U subformula
 	      { $$ = new binop(binop::U, $1, $3); }
-            | subformulae OP_R subformulae
+            | subformula OP_R subformula
 	      { $$ = new binop(binop::R, $1, $3); }
-            | OP_F subformulae
+            | OP_F subformula
 	      { $$ = new unop(unop::F, $2); }
-            | OP_G subformulae
+            | OP_G subformula
 	      { $$ = new unop(unop::G, $2); }
-            | OP_X subformulae
+            | OP_X subformula
 	      { $$ = new unop(unop::X, $2); }
-//	    | subformulae many_errors
+//	    | subformula many_errors
 //              { error_list->push_back(parse_error(@2, 
 //		  "ignoring these unexpected trailing tokens")); 
 //	        $$ = $1;
@@ -155,7 +155,7 @@ yy::Parser::error_()
   error_list->push_back(parse_error(location, message));
 }
 
-formulae* result = 0;
+formula* result = 0;
 
 namespace spot
 {
@@ -163,7 +163,7 @@ namespace spot
   {
     parse_error_list* error_list;
 
-    formulae*
+    formula*
     parse(const std::string& ltl_string, 
 	  parse_error_list& error_list,
 	  bool debug)
diff --git a/src/ltlparse/public.hh b/src/ltlparse/public.hh
index 0a3976081..1a13553cc 100644
--- a/src/ltlparse/public.hh
+++ b/src/ltlparse/public.hh
@@ -2,7 +2,7 @@
 # define SPOT_LTLPARSE_PUBLIC_HH
 
 # include <string>
-# include "ltlast/formulae.hh"
+# include "ltlast/formula.hh"
 # include "location.hh"
 # include <list>
 # include <utility>
@@ -16,7 +16,7 @@ namespace spot
     typedef std::list<parse_error> parse_error_list;
 
     // Beware: this function is *not* reentrant.
-    formulae* parse(const std::string& ltl_string, 
+    formula* parse(const std::string& ltl_string, 
 		    parse_error_list& error_list,
 		    bool debug = false);
 
diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc
index 9cd4f1c5e..4acd2e232 100644
--- a/src/ltltest/equals.cc
+++ b/src/ltltest/equals.cc
@@ -5,7 +5,7 @@
 void
 syntax(char *prog)
 {
-  std::cerr << prog << " formulae1 formulae2" << std::endl;
+  std::cerr << prog << " formula1 formula2" << std::endl;
   exit(2);
 }
 
@@ -17,13 +17,13 @@ main(int argc, char **argv)
 
   
   spot::ltl::parse_error_list p1;
-  spot::ltl::formulae *f1 = spot::ltl::parse(argv[1], p1);
+  spot::ltl::formula *f1 = spot::ltl::parse(argv[1], p1);
 
   if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
     return 2;
 
   spot::ltl::parse_error_list p2;
-  spot::ltl::formulae *f2 = spot::ltl::parse(argv[2], p2);
+  spot::ltl::formula *f2 = spot::ltl::parse(argv[2], p2);
 			
   if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
     return 2;
diff --git a/src/ltltest/readltl.cc b/src/ltltest/readltl.cc
index 64e84588b..4e7486bc3 100644
--- a/src/ltltest/readltl.cc
+++ b/src/ltltest/readltl.cc
@@ -6,7 +6,7 @@
 void
 syntax(char *prog)
 {
-  std::cerr << prog << " [-d] formulae" << std::endl;
+  std::cerr << prog << " [-d] formula" << std::endl;
   exit(2);
 }
 
@@ -19,23 +19,23 @@ main(int argc, char **argv)
     syntax(argv[0]);
 
   bool debug = false;
-  int formulae_index = 1;
+  int formula_index = 1;
 
   if (!strcmp(argv[1], "-d"))
     {
       debug = true;
       if (argc < 3)
 	syntax(argv[0]);
-      formulae_index = 2;
+      formula_index = 2;
     }    
   
   spot::ltl::parse_error_list pel;
-  spot::ltl::formulae *f = spot::ltl::parse(argv[formulae_index], 
+  spot::ltl::formula *f = spot::ltl::parse(argv[formula_index], 
 					    pel, debug);
 
   spot::ltl::parse_error_list::iterator it;
   exit_code = 
-    spot::ltl::format_parse_errors(std::cerr, argv[formulae_index], pel);
+    spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel);
 
   if (f)
     {
diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc
index d5a72687c..d9b213713 100644
--- a/src/ltlvisit/dotty.cc
+++ b/src/ltlvisit/dotty.cc
@@ -95,7 +95,7 @@ namespace spot
     };
 
     void 
-    dotty(const formulae& f, std::ostream& os)
+    dotty(const formula& f, std::ostream& os)
     {
       dotty_visitor v(os);
       os << "digraph G {" << std::endl;
diff --git a/src/ltlvisit/dotty.hh b/src/ltlvisit/dotty.hh
index 48ed2e62d..88bc4644b 100644
--- a/src/ltlvisit/dotty.hh
+++ b/src/ltlvisit/dotty.hh
@@ -1,14 +1,14 @@
 #ifndef SPOT_LTLVISIT_DOTTY_HH
 # define SPOT_LTLVISIT_DOTTY_HH
 
-#include <ltlast/formulae.hh>
+#include <ltlast/formula.hh>
 #include <iostream>
 
 namespace spot 
 {
   namespace ltl
   {
-    void dotty(const formulae& f, std::ostream& os);
+    void dotty(const formula& f, std::ostream& os);
   }
 }
 
diff --git a/src/ltlvisit/dump.cc b/src/ltlvisit/dump.cc
index 712e17992..52c851397 100644
--- a/src/ltlvisit/dump.cc
+++ b/src/ltlvisit/dump.cc
@@ -69,7 +69,7 @@ namespace spot
     };
 
     void 
-    dump(const formulae& f, std::ostream& os)
+    dump(const formula& f, std::ostream& os)
     {
       dump_visitor v(os);
       f.accept(v);
diff --git a/src/ltlvisit/dump.hh b/src/ltlvisit/dump.hh
index d375fd3d7..c1ef7cf29 100644
--- a/src/ltlvisit/dump.hh
+++ b/src/ltlvisit/dump.hh
@@ -1,14 +1,14 @@
 #ifndef SPOT_LTLVISIT_DUMP_HH
 # define SPOT_LTLVISIT_DUMP_HH
 
-#include <ltlast/formulae.hh>
+#include <ltlast/formula.hh>
 #include <iostream>
 
 namespace spot 
 {
   namespace ltl
   {
-    void dump(const formulae& f, std::ostream& os);
+    void dump(const formula& f, std::ostream& os);
   }
 }
 
diff --git a/src/ltlvisit/equals.cc b/src/ltlvisit/equals.cc
index 28c1572f7..915f606f9 100644
--- a/src/ltlvisit/equals.cc
+++ b/src/ltlvisit/equals.cc
@@ -6,7 +6,7 @@ namespace spot
 {
   namespace ltl
   {
-    equals_visitor::equals_visitor(const formulae* f)
+    equals_visitor::equals_visitor(const formula* f)
       : f_(f), result_(false)
     {
     }
@@ -84,7 +84,7 @@ namespace spot
       for (unsigned nf = 0; nf < m_size; ++nf)
 	{
 	  unsigned np;
-	  const formulae* mnth = m->nth(nf);
+	  const formula* mnth = m->nth(nf);
 	  for (np = 0; np < p_size; ++np)
 	    {
 	      if (equals(p->nth(np), mnth))
@@ -94,7 +94,7 @@ namespace spot
 		}
 	    }
 	  // We we haven't found mnth in any child of p, then
-	  // the two formulaes aren't equal.
+	  // the two formulas aren't equal.
 	  if (np == p_size)
 	    return;
 	}
@@ -114,7 +114,7 @@ namespace spot
 	  
 	  // Compare with marked children.
 	  unsigned np2;
-	  const formulae *pnth = p->nth(np);
+	  const formula *pnth = p->nth(np);
 	  for (np2 = 0; np2 < p_size; ++np2)
 	    if (p_seen[np2] && equals(p->nth(np2), pnth))
 	      break;
@@ -124,13 +124,13 @@ namespace spot
 	    return;
 	}
       
-      // The two formulaes match.
+      // The two formulas match.
       result_ = true;
     }
 
 
     bool 
-    equals(const formulae* f1, const formulae* f2)
+    equals(const formula* f1, const formula* f2)
     {
       equals_visitor v(f1);
       f2->accept(v);
diff --git a/src/ltlvisit/equals.hh b/src/ltlvisit/equals.hh
index 704093d9e..2c292302c 100644
--- a/src/ltlvisit/equals.hh
+++ b/src/ltlvisit/equals.hh
@@ -1,4 +1,4 @@
-#include "ltlast/formulae.hh"
+#include "ltlast/formula.hh"
 #include "ltlast/visitor.hh"
 
 namespace spot 
@@ -10,11 +10,11 @@ namespace spot
     class equals_visitor : public const_visitor
     {
     public:
-      equals_visitor(const formulae* f);
+      equals_visitor(const formula* f);
       virtual ~equals_visitor();
 
       // Return true iff the visitor has visited a
-      // formulae which is equal to `f'.
+      // formula which is equal to `f'.
       bool result() const;
       
       void visit(const atomic_prop* ap);
@@ -24,11 +24,11 @@ namespace spot
       void visit(const constant* c);
 	
     private:
-      const formulae* f_;
+      const formula* f_;
       bool result_;
 	      
     };
 
-    bool equals(const formulae* f1, const formulae* f2);
+    bool equals(const formula* f1, const formula* f2);
   }
 }