diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 7 |
2 files changed, 13 insertions, 6 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 56f84d0ff0..b410833d25 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -194,14 +194,14 @@ Program Fixpoint The optional order annotation follows the grammar: .. productionlist:: orderannot - order : measure `term` (`term`)? | wf `term` `term` + order : measure `term` [ `term` ] | wf `term` `ident` - + :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on - any subset of the arguments and the optional (parenthesised) term - ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` - to ``lt``. + + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional term + :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R` + to :g:`lt`. - + :g:`wf R x` which is equivalent to :g:`measure x (R)`. + + :g:`wf R x` which is equivalent to :g:`measure x R`. The structural fixpoint operator behaves just like the one of |Coq| (see :cmd:`Fixpoint`), except it may also generate obligations. It works diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index eebf1f11e1..bdda35fcc0 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -210,6 +210,13 @@ and ``coqtop``, unless stated otherwise: is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems. +:-set *string*: Enable flags and set options. *string* should be + ``Option Name=value``, the value is interpreted according to the + type of the option. For flags ``Option Name`` is equivalent to + ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` + will enable :flag:`Universe Polymorphism`. Note that the quotes are + shell syntax, Coq does not see them. +:-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. :-dump-glob *file*: Dump references for global names in file *file* |