diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala
index a35924d04e4d53721b0450b4464290091d1adcf7..9e4a1332e7044649ddd0434ccecd1e57158bc253 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -1,6 +1,43 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-/** Core package of the Inox solving interface */
+/** Core package of the Inox solving interface
+  *
+  * ==Structure==
+  * 
+  * Leon is organized similarly to a compiler with a concept of [[leon.Pipeline]]
+  * and [[leon.LeonPhase]]. The main phases of Leon are implemented in subpackages, with
+  * an overview of the role of each of them below.
+  * 
+  * The definition of the Pure Scala AST is in [[leon.purescala]]. Most of the other packages
+  * are articulated around the definitions of these ASTs. The [[leon.xlang]] provides extensions
+  * to the Pure Scala AST, but most of the other packages will ignore these extensions and
+  * assume a Pure Scala only AST.
+  * 
+  *   - [[leon.codegen]] provides bytecode generator for Leon programs. Enable the conversion of a [[leon.purescala.Definitions.Program]] to JVM bytecode.
+  * 
+  *   - [[leon.datagen]] provides a generator of expressions (trees), based on vanuatoo.
+  * 
+  *   - [[leon.evaluators]] implements different evaluators for Leon programs in Pure Scala. 
+  * 
+  *   - [[leon.frontends]] provides the different front-ends to Leon. Currently it only implements a scalac integration, but it could potentially support other language.
+  * 
+  *   - [[leon.purescala]] defines the core AST for Pure Scala. Also provides useful tree manipulation methods.
+  * 
+  *   - [[leon.repair]] implements the Repair module of Leon.
+  * 
+  *   - [[leon.solvers]] provides an interface and implementations to solvers for Pure Scala expressions. The solvers are typically wrappers around SMT solvers, with some additional algorithms to handle recursive function invocations.
+  * 
+  *   - [[leon.synthesis]] implements the Synthesis module of Leon.
+  * 
+  *   - [[leon.termination]] implements the termination checker of Leon.
+  * 
+  *   - [[leon.utils]]
+  * 
+  *   - [[leon.verification]] implements the verification module of Leon.
+  * 
+  *   - [[leon.xlang]] provides extensions to Pure Scala. In particular, it introduces some expressions to represent imperative programs. Also provides the code to map such programs to Pure Scala equivalent ones.
+  *
+  */
 package object inox {
   implicit class BooleanToOption(cond: Boolean) {
     def option[A](v: => A) = if (cond) Some(v) else None
diff --git a/src/main/scala/root-doc.txt b/src/main/scala/root-doc.txt
deleted file mode 100644
index 9f01546cc61ad0c4122a05b89fe16d4cdc3e95e4..0000000000000000000000000000000000000000
--- a/src/main/scala/root-doc.txt
+++ /dev/null
@@ -1,37 +0,0 @@
-This is the documentation for the Leon system
-
-==Structure==
-
-Leon is organized similarly to a compiler with a concept of [[leon.Pipeline]]
-and [[leon.LeonPhase]]. The main phases of Leon are implemented in subpackages, with
-an overview of the role of each of them below.
-
-The definition of the Pure Scala AST is in [[leon.purescala]]. Most of the other packages
-are articulated around the definitions of these ASTs. The [[leon.xlang]] provides extensions
-to the Pure Scala AST, but most of the other packages will ignore these extensions and
-assume a Pure Scala only AST.
-
-  - [[leon.codegen]] provides bytecode generator for Leon programs. Enable the conversion of a [[leon.purescala.Definitions.Program]] to JVM bytecode.
-
-  - [[leon.datagen]] provides a generator of expressions (trees), based on vanuatoo.
-
-  - [[leon.evaluators]] implements different evaluators for Leon programs in Pure Scala. 
-
-  - [[leon.frontends]] provides the different front-ends to Leon. Currently it only implements a scalac integration, but it could potentially support other language.
-
-  - [[leon.purescala]] defines the core AST for Pure Scala. Also provides useful tree manipulation methods.
-
-  - [[leon.repair]] implements the Repair module of Leon.
-
-  - [[leon.solvers]] provides an interface and implementations to solvers for Pure Scala expressions. The solvers are typically wrappers around SMT solvers, with some additional algorithms to handle recursive function invocations.
-
-  - [[leon.synthesis]] implements the Synthesis module of Leon.
-
-  - [[leon.termination]] implements the termination checker of Leon.
-
-  - [[leon.utils]]
-
-  - [[leon.verification]] implements the verification module of Leon.
-
-  - [[leon.xlang]] provides extensions to Pure Scala. In particular, it introduces some expressions to represent imperative programs. Also provides the code to map such programs to Pure Scala equivalent ones.
-