diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 0e87e34fa56efd7c263e13e99a95a2d9da122acf..497e729eb9a1a553ee1aa98e504f0a8e78e29764 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -15,7 +15,7 @@ abstract class LeonOptionDef[+A] {
     else s"--$name=$usageRhs"
   }
   def helpString = {
-    f"$usageDesc%-22s" + description.replaceAll("\n", "\n" + " " * 22)
+    f"$usageDesc%-26s" + description.replaceAll("\n", "\n" + " " * 26)
   }
 
   private def parseValue(s: String)(implicit reporter: Reporter): A = {
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 4d525fbcbea9050afda195a0ef9f59c0618b5ae5..66a54ec4cfb1b89be398731d182e1160dbcf6dcb 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -51,19 +51,20 @@ object Main {
   lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
 
   def displayHelp(reporter: Reporter, error: Boolean) = {
-    reporter.info(MainComponent.description)
+
+    reporter.title(MainComponent.description)
     for (opt <- MainComponent.definedOptions.toSeq.sortBy(_.name)) {
       reporter.info(opt.helpString)
     }
     reporter.info("")
 
-    reporter.info("Additional top-level options")
+    reporter.title("Additional top-level options")
     for (opt <- SharedOptions.definedOptions.toSeq.sortBy(_.name)) {
       reporter.info(opt.helpString)
     }
     reporter.info("")
       
-    reporter.info("Additional options, by component:")
+    reporter.title("Additional options, by component:")
 
     for (c <- (allComponents - MainComponent - SharedOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
       reporter.info("")
@@ -77,7 +78,7 @@ object Main {
   }
 
   def displayVersion(reporter: Reporter) = {
-    reporter.info("Leon verification and synthesis tool (http://leon.epfl.ch/)")
+    reporter.title("Leon verification and synthesis tool (http://leon.epfl.ch/)")
     reporter.info("")
   }
 
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 32a920716f91c608126ea596bffeb130718b1936..f4190a113fc0d5153b14726999add15085826dbb 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -43,6 +43,7 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
   final def info(pos: Position, msg: Any): Unit    = emit(account(Message(INFO, pos, msg)))
   final def warning(pos: Position, msg: Any): Unit = emit(account(Message(WARNING, pos, msg)))
   final def error(pos: Position, msg: Any): Unit   = emit(account(Message(ERROR, pos, msg)))
+  final def title(pos: Position, msg: Any): Unit   = emit(account(Message(INFO, pos, Console.BOLD + msg + Console.RESET)))
 
   final def fatalError(pos: Position, msg: Any): Nothing = {
     emit(account(Message(FATAL, pos, msg)))
@@ -97,6 +98,7 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
   final def info(msg: Any): Unit          = info(NoPosition, msg)
   final def warning(msg: Any): Unit       = warning(NoPosition, msg)
   final def error(msg: Any): Unit         = error(NoPosition, msg)
+  final def title(msg: Any): Unit         = title(NoPosition, msg)
   final def fatalError(msg: Any): Nothing = fatalError(NoPosition, msg)
   final def internalError(msg: Any) : Nothing = internalError(NoPosition, msg)
   final def internalAssertion(cond : Boolean, msg: Any) : Unit = internalAssertion(cond,NoPosition, msg)
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index 5c2cce35e885b8be7b27b575a787a3ae51c10976..cbddcd015c07cb279ff7505d27b2851cb27b065d 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -22,7 +22,7 @@ object SharedOptions extends LeonComponent {
     val usageRhs = "f1,f2,..."
   }
 
-  val optEval = LeonStringOptionDef("eval", "Evaluate ground functions", "default", "--eval[=code|default]")
+  val optEval = LeonStringOptionDef("eval", "Evaluate ground functions", "default", "[code|default]")
 
   val optSelectedSolvers = new LeonOptionDef[Set[String]] {
     val name = "solvers"