1 files changed, 63 insertions, 4 deletions

diff --git a/docs/layout-of-source-files.rst b/docs/layout-of-source-files.rst
index b88e7e45..d89ecded 100644
--- a/docs/layout-of-source-files.rst
+++ b/docs/layout-of-source-files.rst
@@ -2,15 +2,29 @@
 Layout of a Solidity Source File
 ********************************
 
-Source files can contain an arbitrary number of contract definitions, include directives
-and pragma directives.
+Source files can contain an arbitrary number of
+:ref:`contract definitions<contract_structure>`, import_ directives
+and :ref:`pragma directives<pragma>`.
+
+.. index:: ! pragma
+
+.. _pragma:
+
+Pragmas
+=======
+
+The ``pragma`` keyword can be used to enable certain compiler features
+or checks. A pragma directive is always local to a source file, so
+you have to add the pragma to all your files if you want enable it
+in all of your project. If you :ref:`import<import>` another file, the pragma
+from that file will not automatically apply to the importing file.
 
 .. index:: ! pragma, version
 
 .. _version_pragma:
 
 Version Pragma
-==============
+--------------
 
 Source files can (and should) be annotated with a so-called version pragma to reject
 being compiled with future compiler versions that might introduce incompatible
@@ -35,6 +49,51 @@ the exact version of the compiler, so that bugfix releases are still possible.
 It is possible to specify much more complex rules for the compiler version,
 the expression follows those used by `npm <https://docs.npmjs.com/misc/semver>`_.
 
+.. note::
+  Using the version pragma will *not* change the version of the compiler.
+  It will also *not* enable or disable features of the compiler. It will just
+  instruct the compiler to check whether its version matches the one
+  required by the pragma. If it does not match, the compiler will issue
+  an error.
+
+.. index:: ! pragma, experimental
+
+.. _experimental_pragma:
+
+Experimental Pragma
+-------------------
+
+The second pragma is the experimental pragma. It can be used to enable
+features of the compiler or language that are not yet enabled by default.
+The following experimental pragmas are currently supported:
+
+
+ABIEncoderV2
+~~~~~~~~~~~~
+
+The new ABI encoder is able to encode and decode arbitrarily nested
+arrays and structs. It produces less optimal code (the optimizer
+for this part of the code is still under development) and has not
+received as much testing as the old encoder. You can activate it
+using ``pragma experimental ABIEncoderV2;``.
+
+SMTChecker
+~~~~~~~~~~
+
+This component has to be enabled when the Solidity compiler is built
+and therefore it is not available in all Solidity binaries.
+The :ref:`build instructions<smt_solvers_build>` explain how to activate this option.
+It is activated for the Ubuntu PPA releases in most versions,
+but not for solc-js, the Docker images, Windows binaries or the
+statically-built Linux binaries.
+
+If you use
+``pragma experimental SMTChecker;``, then you get additional
+safety warnings which are obtained by querying an SMT solver.
+The component does not yet support all features of the Solidity language
+and likely outputs many warnings. In case it reports unsupported
+features, the analysis may not be fully sound.
+
 .. index:: source file, ! import
 
 .. _import:
@@ -215,7 +274,7 @@ for the two input parameters and two returned values.
 
 ::
 
-    pragma solidity ^0.4.0;
+    pragma solidity >=0.4.0 <0.6.0;
 
     /** @title Shape calculator. */
     contract ShapeCalculator {