diff --git a/doc/options.rst b/doc/options.rst index 8d711c7a829f85b2d3b3fec23016040d4dc056f0..02f990fb3a35913beafe0993d29145b42901f100 100644 --- a/doc/options.rst +++ b/doc/options.rst @@ -39,11 +39,6 @@ These options are mutually exclusive. By default, ``--verify`` is chosen. Runs termination analysis. Can be used along ``--verify``. -* ``--xlang`` - - Transforms a program written in the :ref:`xlang` language extension into a :ref:`purescala` program, - then runs program verification. - * ``--noop`` Runs the program through the extraction and preprocessing phases, then outputs it in the specified @@ -176,6 +171,11 @@ These options are available by all Leon components: Set a timeout for each attempt to prove one verification condition/ repair one function (in sec.) +* ``--xlang`` + + Support for additional language constructs described in :ref:`xlang`. + These constructs are desugared into :ref:`purescala` before other operations. + Additional Options, by Component: ---------------------------------