diff --git a/doc/index.rst b/doc/index.rst
index 9ffe65702d89d8cf1ad5cce2c3d7ecc396de9887..bb9f6450902d3f683b2acc1c456fff953ec5d6b1 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -15,6 +15,7 @@ Contents:
    installation
    gettingstarted
    purescala
+   xlang
    verification
    synthesis
    repair
@@ -27,4 +28,3 @@ Indices and tables
 * :ref:`genindex`
 * :ref:`modindex`
 * :ref:`search`
-
diff --git a/doc/xlang.rst b/doc/xlang.rst
new file mode 100644
index 0000000000000000000000000000000000000000..760afbb22cf5f67063825914e4201ec2018b8aff
--- /dev/null
+++ b/doc/xlang.rst
@@ -0,0 +1,55 @@
+.. _xlang:
+
+XLang
+=====
+
+To complement the core PureScala language, the XLang module of Leon brings a
+few extensions to that core language.
+
+These extensions are kept as an optional feature, that needs to be explicitly
+enabled from the command line with the option ``--xlang``. If you do not specify
+the option, Leon will reject any program making use of an XLang feature.
+
+Technically, these extensions are implemented using a translation to PureScala.
+This means They are not implemented in the back-end solving system of Leon, but
+parsed in the the front-end and eliminate early during the Leon pipelining
+process.
+
+Imperative Code
+---------------
+
+XLang lets you introduce local variables in functions, and use Scala assignments
+syntax.
+
+.. code-block:: scala
+
+   def foo(x: Int): Int = {
+     var a = x
+     var b = 42
+     a = a + b
+     b = a
+     b
+   }
+
+The above example illustrates three new features introduced by XLang:
+
+1. Declaring a variable in a local scope
+
+2. Blocks of statement
+
+3. Assignment
+
+
+While loops 
+
+Arrays
+
+Nested function closure on local variables.
+
+.. note::
+   some note comes here
+
+Epsilon
+-------
+
+