diff --git a/ChangeLog b/ChangeLog
index 724d1cac2..742f775ce 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,20 @@
+2004-05-30  Alexandre Duret-Lutz  <adl@gnu.org>
+
+	* src/ltlvisit/forminf.cc (form_eventual_universal_visitor,
+	inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename
+	as ...
+	(eventual_universal_visitor, inf_right_recurse_visitor,
+	inf_left_recurse_visitor): ... these.
+	(is_GF, is_FG): Move ...
+	* src/ltlvisit/basereduc.cc (is_GF, is_FG): ... here, since they
+	are only used here.
+	(basic_reduce_form, basic_reduce_form_visitor): Rename as ...
+	(basic_reduce, basic_reduce_visitor): ... these.
+	* src/ltlvisit/reducform.cc (reduce_form_visitor): Rename as ...
+	(reduce_visitor): ... this.
+	* src/ltltest/inf.cc: Adjust calls.
+	* src/sanity/style.test: Improve missing-space after coma detection.
+
 2004-05-26  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/ltlvisit/reducform.cc (reduce_form_visitor::visit(constant)):
diff --git a/src/ltltest/inf.cc b/src/ltltest/inf.cc
index a715cb39f..c2e68ae99 100644
--- a/src/ltltest/inf.cc
+++ b/src/ltltest/inf.cc
@@ -68,7 +68,7 @@ main(int argc, char** argv)
     {
     case 0:
       std::cout << "Test f1 < f2" << std::endl;
-      if (spot::ltl::inf_form(f1, f2))
+      if (spot::ltl::syntactic_implication(f1, f2))
 	{
 	  std::cout << f1s << " < " << f2s << std::endl;
 	  exit_return = 1;
@@ -77,7 +77,7 @@ main(int argc, char** argv)
 
     case 1:
       std::cout << "Test !f1 < f2" << std::endl;
-      if (spot::ltl::infneg_form(f1, f2, 0))
+      if (spot::ltl::syntactic_implication_neg(f1, f2, false))
 	{
 	  std::cout << "!(" << f1s << ") < " << f2s << std::endl;
 	  exit_return = 1;
@@ -86,7 +86,7 @@ main(int argc, char** argv)
 
     case 2:
       std::cout << "Test f1 < !f2" << std::endl;
-      if (spot::ltl::infneg_form(f1, f2, 1))
+      if (spot::ltl::syntactic_implication_neg(f1, f2, true))
 	{
 	  std::cout << f1s << " < !(" << f2s << ")" << std::endl;
 	  exit_return = 1;
@@ -96,8 +96,8 @@ main(int argc, char** argv)
       break;
     }
 
-  spot::ltl::dump(std::cout, f1); std::cout << std::endl;
-  spot::ltl::dump(std::cout, f2); std::cout << std::endl;
+  spot::ltl::dump(std::cout, f1) << std::endl;
+  spot::ltl::dump(std::cout, f2) << std::endl;
 
   spot::ltl::destroy(f1);
   spot::ltl::destroy(f2);
diff --git a/src/ltlvisit/basereduc.cc b/src/ltlvisit/basereduc.cc
index b488c580d..c80b89f60 100644
--- a/src/ltlvisit/basereduc.cc
+++ b/src/ltlvisit/basereduc.cc
@@ -29,13 +29,42 @@ namespace spot
 {
   namespace ltl
   {
-    class basic_reduce_form_visitor : public visitor
+
+    bool
+    is_GF(const formula* f)
+    {
+      const unop* op = dynamic_cast<const unop*>(f);
+      if (op && op->op() == unop::G)
+	{
+	  const unop* opchild = dynamic_cast<const unop*>(op->child());
+	  if (opchild && opchild->op() == unop::F)
+	    return true;
+	}
+      return false;
+    }
+
+    bool
+    is_FG(const formula* f)
+    {
+      const unop* op = dynamic_cast<const unop*>(f);
+      if (op && op->op() == unop::F)
+	{
+	  const unop* opchild = dynamic_cast<const unop*>(op->child());
+	  if (opchild && opchild->op() == unop::G)
+	    return true;
+	}
+      return false;
+    }
+
+    formula* basic_reduce(const formula* f);
+
+    class basic_reduce_visitor : public visitor
     {
     public:
 
-      basic_reduce_form_visitor(){}
+      basic_reduce_visitor(){}
 
-      virtual ~basic_reduce_form_visitor(){}
+      virtual ~basic_reduce_visitor(){}
 
       formula*
       result() const
@@ -60,7 +89,7 @@ namespace spot
       visit(unop* uo)
       {
 	formula* f = uo->child();
-	result_ = basic_reduce_form(f);
+	result_ = basic_reduce(f);
 	multop* mo = NULL;
 	unop* u = NULL;
 	binop* bo = NULL;
@@ -90,10 +119,9 @@ namespace spot
 		if (is_GF(mo->nth(0)))
 		  {
 		    multop::vec* res = new multop::vec;
-		    res->push_back
-		      (unop::instance(unop::F,
-				      basic_reduce_form(mo->nth(1))));
-		    res->push_back(basic_reduce_form(mo->nth(0)));
+		    res->push_back(unop::instance(unop::F,
+						  basic_reduce(mo->nth(1))));
+		    res->push_back(basic_reduce(mo->nth(0)));
 		    result_ = multop::instance(mo->op(), res);
 		    destroy(mo);
 		    return;
@@ -101,10 +129,9 @@ namespace spot
 		if (is_GF(mo->nth(1)))
 		  {
 		    multop::vec* res = new multop::vec;
-		    res->push_back
-		      (unop::instance(unop::F,
-				      basic_reduce_form(mo->nth(0))));
-		    res->push_back(basic_reduce_form(mo->nth(1)));
+		    res->push_back(unop::instance(unop::F,
+						  basic_reduce(mo->nth(0))));
+		    res->push_back(basic_reduce(mo->nth(1)));
 		    result_ = multop::instance(mo->op(), res);
 		    destroy(mo);
 		    return;
@@ -127,7 +154,7 @@ namespace spot
 		result_ =
 		  unop::instance(unop::X,
 				 unop::instance(unop::F,
-						basic_reduce_form(u->child())));
+						basic_reduce(u->child())));
 		destroy(u);
 	      return;
 	    }
@@ -142,10 +169,9 @@ namespace spot
 		if (is_GF(mo->nth(0)))
 		  {
 		    multop::vec* res = new multop::vec;
-		    res->push_back
-		      (unop::instance(unop::F,
-				      basic_reduce_form(mo->nth(1))));
-		    res->push_back(basic_reduce_form(mo->nth(0)));
+		    res->push_back(unop::instance(unop::F,
+						  basic_reduce(mo->nth(1))));
+		    res->push_back(basic_reduce(mo->nth(0)));
 		    result_ = multop::instance(mo->op(), res);
 		    destroy(mo);
 		    return;
@@ -153,10 +179,9 @@ namespace spot
 		if (is_GF(mo->nth(1)))
 		  {
 		    multop::vec* res = new multop::vec;
-		    res->push_back
-		      (unop::instance(unop::F,
-				      basic_reduce_form(mo->nth(0))));
-		    res->push_back(basic_reduce_form(mo->nth(1)));
+		    res->push_back(unop::instance(unop::F,
+						  basic_reduce(mo->nth(0))));
+		    res->push_back(basic_reduce(mo->nth(1)));
 		    result_ = multop::instance(mo->op(), res);
 		    destroy(mo);
 		    return;
@@ -178,7 +203,7 @@ namespace spot
 	    if (bo && bo->op() == binop::R)
 	      {
 		result_ = unop::instance(unop::G,
-					 basic_reduce_form(bo->second()));
+					 basic_reduce(bo->second()));
 		destroy(bo);
 		return;
 	      }
@@ -190,7 +215,7 @@ namespace spot
 		result_ =
 		  unop::instance(unop::X,
 				 unop::instance(unop::G,
-						basic_reduce_form(u->child())));
+						basic_reduce(u->child())));
 		destroy(u);
 		return;
 	      }
@@ -205,10 +230,9 @@ namespace spot
 		if (is_GF(mo->nth(0)))
 		  {
 		    multop::vec* res = new multop::vec;
-		    res->push_back
-		      (unop::instance(unop::F,
-				      basic_reduce_form(mo->nth(1))));
-		    res->push_back(basic_reduce_form(mo->nth(0)));
+		    res->push_back(unop::instance(unop::F,
+						  basic_reduce(mo->nth(1))));
+		    res->push_back(basic_reduce(mo->nth(0)));
 		    result_ = multop::instance(mo->op(), res);
 		    destroy(mo);
 		    return;
@@ -216,10 +240,9 @@ namespace spot
 		if (is_GF(mo->nth(1)))
 		  {
 		    multop::vec* res = new multop::vec;
-		    res->push_back
-		      (unop::instance(unop::F,
-				      basic_reduce_form(mo->nth(0))));
-		    res->push_back(basic_reduce_form(mo->nth(1)));
+		    res->push_back(unop::instance(unop::F,
+						  basic_reduce(mo->nth(0))));
+		    res->push_back(basic_reduce(mo->nth(1)));
 		    result_ = multop::instance(mo->op(), res);
 		    destroy(mo);
 		    return;
@@ -245,21 +268,21 @@ namespace spot
 	  {
 	  case binop::Xor:
 	    result_ = binop::instance(binop::Xor,
-				      basic_reduce_form(f1),
-				      basic_reduce_form(f2));
+				      basic_reduce(f1),
+				      basic_reduce(f2));
 	    return;
 	  case binop::Equiv:
 	    result_ = binop::instance(binop::Equiv,
-				      basic_reduce_form(f1),
-				      basic_reduce_form(f2));
+				      basic_reduce(f1),
+				      basic_reduce(f2));
 	    return;
 	  case binop::Implies:
 	    result_ = binop::instance(binop::Implies,
-				      basic_reduce_form(f1),
-				      basic_reduce_form(f2));
+				      basic_reduce(f1),
+				      basic_reduce(f2));
 	    return;
 	  case binop::U:
-	    f2 = basic_reduce_form(f2);
+	    f2 = basic_reduce(f2);
 
 	    // a U false = false
 	    // a U true = true
@@ -269,7 +292,7 @@ namespace spot
 		return;
 	      }
 
-	    f1 = basic_reduce_form(f1);
+	    f1 = basic_reduce(f1);
 
 	    // X(a) U X(b) = X(a U b)
 	    fu1 = dynamic_cast<unop*>(f1);
@@ -279,9 +302,9 @@ namespace spot
 		(fu2->op() == unop::X))
 	      {
 		ftmp = binop::instance(binop::U,
-				       basic_reduce_form(fu1->child()),
-				       basic_reduce_form(fu2->child()));
-		result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
+				       basic_reduce(fu1->child()),
+				       basic_reduce(fu2->child()));
+		result_ = unop::instance(unop::X, basic_reduce(ftmp));
 		destroy(f1);
 		destroy(f2);
 		destroy(ftmp);
@@ -292,7 +315,7 @@ namespace spot
 	    return;
 
 	  case binop::R:
-	    f2 = basic_reduce_form(f2);
+	    f2 = basic_reduce(f2);
 
 	    // a R false = false
 	    // a R true = true
@@ -302,7 +325,7 @@ namespace spot
 		return;
 	      }
 
-	    f1 = basic_reduce_form(f1);
+	    f1 = basic_reduce(f1);
 
 	    // X(a) R X(b) = X(a R b)
 	    fu1 = dynamic_cast<unop*>(f1);
@@ -312,9 +335,9 @@ namespace spot
 		(fu2->op() == unop::X))
 	      {
 		ftmp = binop::instance(bo->op(),
-				       basic_reduce_form(fu1->child()),
-				       basic_reduce_form(fu2->child()));
-		result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
+				       basic_reduce(fu1->child()),
+				       basic_reduce(fu2->child()));
+		result_ = unop::instance(unop::X, basic_reduce(ftmp));
 		destroy(f1);
 		destroy(f2);
 		destroy(ftmp);
@@ -349,7 +372,7 @@ namespace spot
 	formula* ftmp = NULL;
 
 	for (unsigned i = 0; i < mos; ++i)
-	  res->push_back(basic_reduce_form(mo->nth(i)));
+	  res->push_back(basic_reduce(mo->nth(i)));
 
 
 	switch (op)
@@ -367,17 +390,17 @@ namespace spot
 		    if (uo && uo->op() == unop::X)
 		      {
 			// Xa & Xb = X(a & b)
-			tmpX->push_back(basic_reduce_form(uo->child()));
+			tmpX->push_back(basic_reduce(uo->child()));
 		      }
 		    else if (is_FG(*i))
 		      {
 			// FG(a) & FG(b) = FG(a & b)
 			unop* uo2 = dynamic_cast<unop*>(uo->child());
-			tmpFG->push_back(basic_reduce_form(uo2->child()));
+			tmpFG->push_back(basic_reduce(uo2->child()));
 		      }
 		    else
 		      {
-			tmpOther->push_back(basic_reduce_form(*i));
+			tmpOther->push_back(basic_reduce(*i));
 		      }
 		  }
 		else if (bo)
@@ -396,7 +419,7 @@ namespace spot
 				&& ftmp == bo2->second())
 			      {
 				tmpUright
-				  ->push_back(basic_reduce_form(bo2->first()));
+				  ->push_back(basic_reduce(bo2->first()));
 				if (j != i)
 				  {
 				    destroy(*j);
@@ -410,7 +433,7 @@ namespace spot
 						      instance(multop::
 							       And,
 							       tmpUright),
-						      basic_reduce_form(ftmp)));
+						      basic_reduce(ftmp)));
 		      }
 		    else if (bo->op() == binop::R)
 		      {
@@ -426,7 +449,7 @@ namespace spot
 				&& ftmp == bo2->first())
 			      {
 				tmpRright
-				  ->push_back(basic_reduce_form(bo2->second()));
+				  ->push_back(basic_reduce(bo2->second()));
 				if (j != i)
 				  {
 				    destroy(*j);
@@ -436,19 +459,19 @@ namespace spot
 			  }
 			tmpR
 			  ->push_back(binop::instance(binop::R,
-						      basic_reduce_form(ftmp),
+						      basic_reduce(ftmp),
 						      multop::
 						      instance(multop::And,
 							       tmpRright)));
 		      }
 		    else
 		      {
-			tmpOther->push_back(basic_reduce_form(*i));
+			tmpOther->push_back(basic_reduce(*i));
 		      }
 		  }
 		else
 		  {
-		    tmpOther->push_back(basic_reduce_form(*i));
+		    tmpOther->push_back(basic_reduce(*i));
 		  }
 		destroy(*i);
 	      }
@@ -471,17 +494,17 @@ namespace spot
 		    if (uo && uo->op() == unop::X)
 		      {
 			// Xa | Xb = X(a | b)
-			tmpX->push_back(basic_reduce_form(uo->child()));
+			tmpX->push_back(basic_reduce(uo->child()));
 		      }
 		    else if (is_GF(*i))
 		      {
 			// GF(a) | GF(b) = GF(a | b)
 			unop* uo2 = dynamic_cast<unop*>(uo->child());
-			tmpGF->push_back(basic_reduce_form(uo2->child()));
+			tmpGF->push_back(basic_reduce(uo2->child()));
 		      }
 		    else
 		      {
-			tmpOther->push_back(basic_reduce_form(*i));
+			tmpOther->push_back(basic_reduce(*i));
 		      }
 		  }
 		else if (bo)
@@ -500,7 +523,7 @@ namespace spot
 				&& ftmp == bo2->first())
 			      {
 				tmpUright
-				  ->push_back(basic_reduce_form(bo2->second()));
+				  ->push_back(basic_reduce(bo2->second()));
 				if (j != i)
 				  {
 				    destroy(*j);
@@ -509,7 +532,7 @@ namespace spot
 			      }
 			  }
 			tmpU->push_back(binop::instance(binop::U,
-							basic_reduce_form(ftmp),
+							basic_reduce(ftmp),
 							multop::
 							instance(multop::Or,
 								 tmpUright)));
@@ -528,7 +551,7 @@ namespace spot
 				&& ftmp == bo2->second())
 			      {
 				tmpRright
-				  ->push_back(basic_reduce_form(bo->first()));
+				  ->push_back(basic_reduce(bo->first()));
 				if (j != i)
 				  {
 				    destroy(*j);
@@ -541,16 +564,16 @@ namespace spot
 						      multop::
 						      instance(multop::Or,
 							       tmpRright),
-						      basic_reduce_form(ftmp)));
+						      basic_reduce(ftmp)));
 		      }
 		    else
 		      {
-			tmpOther->push_back(basic_reduce_form(*i));
+			tmpOther->push_back(basic_reduce(*i));
 		      }
 		  }
 		else
 		  {
-		    tmpOther->push_back(basic_reduce_form(*i));
+		    tmpOther->push_back(basic_reduce(*i));
 		  }
 		destroy(*i);
 	      }
@@ -610,9 +633,10 @@ namespace spot
       formula* result_;
     };
 
-    formula* basic_reduce_form(const formula* f)
+    formula*
+    basic_reduce(const formula* f)
     {
-      basic_reduce_form_visitor v;
+      basic_reduce_visitor v;
       const_cast<formula*>(f)->accept(v);
       return v.result();
     }
diff --git a/src/ltlvisit/forminf.cc b/src/ltlvisit/forminf.cc
index 5589cf739..0a1b20025 100644
--- a/src/ltlvisit/forminf.cc
+++ b/src/ltlvisit/forminf.cc
@@ -32,43 +32,17 @@ namespace spot
   namespace ltl
   {
 
-    bool
-    is_GF(const formula* f)
-    {
-      const unop* op = dynamic_cast<const unop*>(f);
-      if (op && op->op() == unop::G)
-	{
-	  const unop* opchild = dynamic_cast<const unop*>(op->child());
-	  if (opchild && opchild->op() == unop::F)
-	    return true;
-	}
-      return false;
-    }
-
-    bool
-    is_FG(const formula* f)
-    {
-      const unop* op = dynamic_cast<const unop*>(f);
-      if (op && op->op() == unop::F)
-	{
-	  const unop* opchild = dynamic_cast<const unop*>(op->child());
-	  if (opchild && opchild->op() == unop::G)
-	    return true;
-	}
-      return false;
-    }
-
-    class form_eventual_universal_visitor : public const_visitor
+    class eventual_universal_visitor : public const_visitor
     {
     public:
 
-      form_eventual_universal_visitor()
+      eventual_universal_visitor()
 	: eventual(false), universal(false)
       {
       }
 
       virtual
-      ~form_eventual_universal_visitor()
+      ~eventual_universal_visitor()
       {
       }
 
@@ -163,7 +137,7 @@ namespace spot
       bool
       recurse_ev(const formula* f)
       {
-	form_eventual_universal_visitor v;
+	eventual_universal_visitor v;
 	const_cast<formula*>(f)->accept(v);
 	return v.is_eventual();
       }
@@ -171,7 +145,7 @@ namespace spot
       bool
       recurse_un(const formula* f)
       {
-	form_eventual_universal_visitor v;
+	eventual_universal_visitor v;
 	const_cast<formula*>(f)->accept(v);
 	return v.is_universal();
       }
@@ -182,33 +156,36 @@ namespace spot
     };
 
 
-    bool is_eventual(const formula* f)
+    bool
+    is_eventual(const formula* f)
     {
-      form_eventual_universal_visitor v;
+      eventual_universal_visitor v;
       const_cast<formula*>(f)->accept(v);
       return v.is_eventual();
     }
 
-    bool is_universal(const formula* f)
+    bool
+    is_universal(const formula* f)
     {
-      form_eventual_universal_visitor v;
+      eventual_universal_visitor v;
       const_cast<formula*>(f)->accept(v);
       return v.is_universal();
     }
 
     /////////////////////////////////////////////////////////////////////////
 
-    class inf_form_right_recurse_visitor : public const_visitor
+
+    class inf_right_recurse_visitor : public const_visitor
     {
     public:
 
-      inf_form_right_recurse_visitor(const formula *f)
+      inf_right_recurse_visitor(const formula *f)
 	: result_(false), f(f)
       {
       }
 
       virtual
-      ~inf_form_right_recurse_visitor()
+      ~inf_right_recurse_visitor()
       {
       }
 
@@ -254,17 +231,17 @@ namespace spot
 	    {
 	      const unop* op = dynamic_cast<const unop*>(f);
 	      if (op && op->op() == unop::X)
-		result_ = inf_form(op->child(), f1);
+		result_ = syntactic_implication(op->child(), f1);
 	    }
 	    return;
 	  case unop::F:
 	    /* F(a) = true U a */
-	    result_ = inf_form(f, f1);
+	    result_ = syntactic_implication(f, f1);
 	    return;
 	  case unop::G:
 	    /* G(a) = false R a */
 	    tmp = constant::false_instance();
-	    if (inf_form(f, tmp))
+	    if (syntactic_implication(f, tmp))
 	      result_ = true;
 	    destroy(tmp);
 	    return;
@@ -285,11 +262,12 @@ namespace spot
 	  case binop::Implies:
 	    return;
 	  case binop::U:
-	    if (inf_form(f, f2))
+	    if (syntactic_implication(f, f2))
 	      result_ = true;
 	    return;
 	  case binop::R:
-	    if (inf_form(f, f1) && inf_form(f, f2))
+	    if (syntactic_implication(f, f1)
+		&& syntactic_implication(f, f2))
 	      result_ = true;
 	    return;
 	  }
@@ -306,13 +284,13 @@ namespace spot
 	  {
 	  case multop::And:
 	    for (unsigned i = 0; i < mos; ++i)
-	      if (!inf_form(f, mo->nth(i)))
+	      if (!syntactic_implication(f, mo->nth(i)))
 		return;
 	    result_ = true;
 	    break;
 	  case multop::Or:
 	    for (unsigned i = 0; i < mos && !result_; ++i)
-	      if (inf_form(f, mo->nth(i)))
+	      if (syntactic_implication(f, mo->nth(i)))
 		result_ = true;
 	    break;
 	  }
@@ -323,7 +301,7 @@ namespace spot
       {
 	if (f1 == f2)
 	  return true;
-	inf_form_right_recurse_visitor v(f2);
+	inf_right_recurse_visitor v(f2);
 	const_cast<formula*>(f1)->accept(v);
 	return v.result();
       }
@@ -335,17 +313,17 @@ namespace spot
 
     /////////////////////////////////////////////////////////////////////////
 
-    class inf_form_left_recurse_visitor : public const_visitor
+    class inf_left_recurse_visitor : public const_visitor
     {
     public:
 
-      inf_form_left_recurse_visitor(const formula *f)
+      inf_left_recurse_visitor(const formula *f)
 	: result_(false), f(f)
       {
       }
 
       virtual
-      ~inf_form_left_recurse_visitor()
+      ~inf_left_recurse_visitor()
       {
       }
 
@@ -355,8 +333,8 @@ namespace spot
 	const binop* fb = dynamic_cast<const binop*>(f);
 	const binop* f2b = dynamic_cast<const binop*>(f2);
 	if (fb && f2b && fb->op() == f2b->op()
-	    && inf_form(f2b->first(), fb->first())
-	    && inf_form(f2b->second(), fb->second()))
+	    && syntactic_implication(f2b->first(), fb->first())
+	    && syntactic_implication(f2b->second(), fb->second()))
 	  return true;
 	return false;
       }
@@ -370,7 +348,7 @@ namespace spot
       void
       visit(const atomic_prop* ap)
       {
-	inf_form_right_recurse_visitor v(ap);
+	inf_right_recurse_visitor v(ap);
 	const_cast<formula*>(f)->accept(v);
 	result_ = v.result();
       }
@@ -378,7 +356,7 @@ namespace spot
       void
       visit(const constant* c)
       {
-	inf_form_right_recurse_visitor v(c);
+	inf_right_recurse_visitor v(c);
 	switch (c->val())
 	  {
 	  case constant::True:
@@ -397,7 +375,7 @@ namespace spot
       visit(const unop* uo)
       {
 	const formula* f1 = uo->child();
-	inf_form_right_recurse_visitor v(uo);
+	inf_right_recurse_visitor v(uo);
 	switch (uo->op())
 	  {
 	  case unop::Not:
@@ -408,7 +386,7 @@ namespace spot
 	    {
 	      const unop* op = dynamic_cast<const unop*>(f);
 	      if (op && op->op() == unop::X)
-		result_ = inf_form(f1, op->child());
+		result_ = syntactic_implication(f1, op->child());
 	    }
 	    return;
 	  case unop::F:
@@ -423,7 +401,7 @@ namespace spot
 		  destroy(tmp);
 		  return;
 		}
-	      if (inf_form(tmp, f))
+	      if (syntactic_implication(tmp, f))
 		result_ = true;
 	      destroy(tmp);
 	      return;
@@ -440,7 +418,7 @@ namespace spot
 		  destroy(tmp);
 		  return;
 		}
-	      if (inf_form(f1, f))
+	      if (syntactic_implication(f1, f))
 		result_ = true;
 	      destroy(tmp);
 	      return;
@@ -468,11 +446,12 @@ namespace spot
 	  case binop::Implies:
 	    return;
 	  case binop::U:
-	    if (inf_form(f1, f) && inf_form(f2, f))
+	    if (syntactic_implication(f1, f)
+		&& syntactic_implication(f2, f))
 	      result_ = true;
 	    return;
 	  case binop::R:
-	    if (inf_form(f2, f))
+	    if (syntactic_implication(f2, f))
 	      result_ = true;
 	    return;
 	  }
@@ -489,12 +468,12 @@ namespace spot
 	  {
 	  case multop::And:
 	    for (unsigned i = 0; (i < mos) && !result_; ++i)
-	      if (inf_form(mo->nth(i), f))
+	      if (syntactic_implication(mo->nth(i), f))
 		result_ = true;
 	    break;
 	  case multop::Or:
 	    for (unsigned i = 0; i < mos; ++i)
-	      if (!inf_form(mo->nth(i), f))
+	      if (!syntactic_implication(mo->nth(i), f))
 		return;
 	    result_ = true;
 	    break;
@@ -506,15 +485,15 @@ namespace spot
       const formula* f;
     };
 
+    // This is called by syntactic_implication() after the
+    // formulae have been normalized.
     bool
-    inf_form(const formula* f1, const formula* f2)
+    syntactic_implication(const formula* f1, const formula* f2)
     {
-      /* f1 and f2 are unabbreviated */
       if (f1 == f2)
 	return true;
-      inf_form_left_recurse_visitor v1(f2);
-      inf_form_right_recurse_visitor v2(f1);
-
+      inf_left_recurse_visitor v1(f2);
+      inf_right_recurse_visitor v2(f1);
 
       if (f2 == constant::true_instance()
 	  || f1 == constant::false_instance())
@@ -532,13 +511,13 @@ namespace spot
     }
 
     bool
-    infneg_form(const formula* f1, const formula* f2, int n)
+    syntactic_implication_neg(const formula* f1, const formula* f2, bool right)
     {
       const formula* ftmp1;
       const formula* ftmp2;
       const formula* ftmp3 = unop::instance(unop::Not,
-					    (!n) ? clone(f1) : clone(f2));
-      const formula* ftmp4 = negative_normal_form((!n) ? f2 : f1);
+					    right ? clone(f2) : clone(f1));
+      const formula* ftmp4 = negative_normal_form(right ? f1 : f2);
       const formula* ftmp5;
       const formula* ftmp6;
       bool result;
@@ -549,10 +528,10 @@ namespace spot
       ftmp5 = unabbreviate_logic(ftmp4);
       ftmp6 = negative_normal_form(ftmp5);
 
-      if (n == 0)
-	result = inf_form(ftmp1, ftmp6);
+      if (right)
+	result = syntactic_implication(ftmp6, ftmp1);
       else
-	result = inf_form(ftmp6, ftmp1);
+	result = syntactic_implication(ftmp1, ftmp6);
 
       destroy(ftmp1);
       destroy(ftmp2);
diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc
index 856fe46f8..d48efb655 100644
--- a/src/ltlvisit/reducform.cc
+++ b/src/ltlvisit/reducform.cc
@@ -32,16 +32,16 @@ namespace spot
   namespace ltl
   {
 
-    class reduce_form_visitor : public visitor
+    class reduce_visitor : public visitor
     {
     public:
 
-      reduce_form_visitor(int opt)
+      reduce_visitor(int opt)
 	: opt_(opt)
       {
       }
 
-      virtual ~reduce_form_visitor()
+      virtual ~reduce_visitor()
       {
       }
 
@@ -116,10 +116,11 @@ namespace spot
 
 	if (opt_ & Reduce_Syntactic_Implications)
 	  {
-	    bool inf = inf_form(f1, f2);
-	    bool infinv = inf_form(f2, f1);
-	    bool infnegleft = infneg_form(f2, f1, 0);
-	    bool infnegright = infneg_form(f2, f1, 1);
+	    // FIXME: These should be done only when needed.
+	    bool inf = syntactic_implication(f1, f2);
+	    bool infinv = syntactic_implication(f2, f1);
+	    bool infnegleft = syntactic_implication_neg(f2, f1, false);
+	    bool infnegright = syntactic_implication_neg(f2, f1, true);
 
 	    switch (bo->op())
 	      {
@@ -146,7 +147,8 @@ namespace spot
 		/* a < b => a U (b U c) = (b U c) */
 		{
 		  binop* bo = dynamic_cast<binop*>(f2);
-		  if (bo && bo->op() == binop::U && inf_form(f1, bo->first()))
+		  if (bo && bo->op() == binop::U
+		      && syntactic_implication(f1, bo->first()))
 		    {
 		      result_ = f2;
 		      destroy(f1);
@@ -173,7 +175,8 @@ namespace spot
 		/* b < a => a R (b R c) = b R c */
 		{
 		  binop* bo = dynamic_cast<binop*>(f2);
-		  if (bo && bo->op() == binop::R && inf_form(bo->first(), f1))
+		  if (bo && bo->op() == binop::R
+		      && syntactic_implication(bo->first(), f1))
 		    {
 		      result_ = f2;
 		      destroy(f1);
@@ -215,7 +218,7 @@ namespace spot
 		  {
 		    f2 = *index;
 		    /* a < b => a + b = b */
-		    if (inf_form(f1, f2)) // f1 < f2
+		    if (syntactic_implication(f1, f2)) // f1 < f2
 		      {
 			f1 = f2;
 			destroy(*indextmp);
@@ -223,7 +226,7 @@ namespace spot
 			indextmp = index;
 			index--;
 		      }
-		    else if (inf_form(f2, f1)) // f2 < f1
+		    else if (syntactic_implication(f2, f1)) // f2 < f1
 		      {
 			destroy(*index);
 			res->erase(index);
@@ -243,13 +246,13 @@ namespace spot
 		  {
 		    f2 = *index;
 		    /* a < b => a & b = a */
-		    if (inf_form(f1, f2)) // f1 < f2
+		    if (syntactic_implication(f1, f2)) // f1 < f2
 		      {
 			destroy(*index);
 			res->erase(index);
 			index--;
 		      }
-		    else if (inf_form(f2, f1)) // f2 < f1
+		    else if (syntactic_implication(f2, f1)) // f2 < f1
 		      {
 			f1 = f2;
 			destroy(*indextmp);
@@ -266,8 +269,8 @@ namespace spot
 	    for (index = res->begin(); index != res->end(); index++)
 	      for (indextmp = res->begin(); indextmp != res->end(); indextmp++)
 		if (index != indextmp
-		    && infneg_form(*index,*indextmp,
-				   (mo->op() == multop::Or) ? 0 : 1))
+		    && syntactic_implication_neg(*index, *indextmp,
+						 mo->op() != multop::Or))
 		  {
 		    for (multop::vec::iterator j = res->begin();
 			 j != res->end(); j++)
@@ -310,27 +313,27 @@ namespace spot
 
       if (opt & Reduce_Basics)
 	{
-	  f1 = basic_reduce_form(f2);
+	  f1 = basic_reduce(f2);
 	  destroy(f2);
 	  f2 = f1;
 	}
       if (opt & (Reduce_Syntactic_Implications
 		 | Reduce_Eventuality_And_Universality))
 	{
-	  reduce_form_visitor v(opt);
+	  reduce_visitor v(opt);
 	  f2->accept(v);
 	  f1 = v.result();
 	  destroy(f2);
 	  f2 = f1;
 
-	  // Run basic_reduce_form again.
+	  // Run basic_reduce again.
 	  //
 	  // Consider `F b & g'   were g is an eventual formula rewritten
-	  // as `g = F c'  Then basic_reduce_form with rewrite it
+	  // as `g = F c'  Then basic_reduce with rewrite it
 	  // as F(b & c).
 	  if (opt & Reduce_Basics)
 	    {
-	      f1 = basic_reduce_form(f2);
+	      f1 = basic_reduce(f2);
 	      destroy(f2);
 	      f2 = f1;
 	    }
diff --git a/src/ltlvisit/reducform.hh b/src/ltlvisit/reducform.hh
index 2fd5a7245..35715daf6 100644
--- a/src/ltlvisit/reducform.hh
+++ b/src/ltlvisit/reducform.hh
@@ -53,16 +53,18 @@ namespace spot
     /// \return the reduced formula
     formula* reduce(const formula* f, int opt = Reduce_All);
 
-    /// Implement basic rewriting.
-    formula* basic_reduce_form(const formula* f);
+    /// Basic rewritings.
+    formula* basic_reduce(const formula* f);
 
-    /// Detect easy case of implies.
-    /// True if f1 < f2, false otherwise.
-    bool inf_form(const formula* f1, const formula* f2);
-    /// Detect easy case of implies.
-    /// If n = 0, true if !f1 < f2, false otherwise.
-    /// If n = 1, true if f1 < !f2, false otherwise.
-    bool infneg_form(const formula* f1, const formula* f2, int n);
+    /// \brief Syntactic implication.
+    bool syntactic_implication(const formula* f1, const formula* f2);
+
+    /// \brief Syntactic implication.
+    ///
+    /// If right==false, true if !f1 < f2, false otherwise.
+    /// If right==true, true if f1 < !f2, false otherwise.
+    bool syntactic_implication_neg(const formula* f1, const formula* f2,
+				   bool right);
 
     /// \brief Check whether a formula is eventual.
     ///
diff --git a/src/sanity/style.test b/src/sanity/style.test
index 1b54d4cd6..2e20410ec 100755
--- a/src/sanity/style.test
+++ b/src/sanity/style.test
@@ -80,7 +80,7 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
     grep '! ' $tmp &&
       diag 'No space after unary operators (!).'
 
-    grep ',[(a-zA-Z+=_!]' $tmp &&
+    grep ',[^ "%]' $tmp &&
       diag 'Space after coma.'
 
     grep '[^	 ]&&[^	 ]' $tmp &&