diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/Translator.tex | 2 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 3 |
2 files changed, 4 insertions, 1 deletions
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index 3ee65d6f22..d8ac640f2a 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -490,7 +490,7 @@ to be applied are separated by a {\tt =>}. to turn implicit only the arguments that are {\em strictly} implicit (or rigid), i.e. that remains inferable whatever the other arguments are. For instance {\tt x} inferable from {\tt P x} is not strictly -inferable since it can disappears if {\tt P} is instanciated by a term +inferable since it can disappears if {\tt P} is instantiated by a term which erases {\tt x}. \begin{transbox} diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index edf4e6ec9d..2c69dcfe08 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -560,6 +560,9 @@ class CoqtopDirective(Directive): Print nat. Definition a := 1. + The blank line after the directive is required. If you begin a proof, + include an ``Abort`` afterwards to reset coqtop for the next example. + Here is a list of permissible options: - Display options |