diff options
| author | Pierre-Marie Pédrot | 2015-10-15 09:47:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-15 09:47:43 +0200 |
| commit | cbd28511526dfb561017c3d27a73598f6ce5f68d (patch) | |
| tree | a8786b32433caa850e24f67ab5a3aa85f29a683a /doc/tools | |
| parent | 10e5883fed21f9631e1aa65adb7a7e62a529987f (diff) | |
| parent | 7402a7788b6a73bd5c0cb9078823d48e6f01a357 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/Translator.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex index 5f7b6dc951..ed1d336d9e 100644 --- a/doc/tools/Translator.tex +++ b/doc/tools/Translator.tex @@ -419,7 +419,7 @@ the hypotheses), or a comma-separated list of either hypothesis name, or {\tt (value of $H$)} or {\tt (type of $H$)}. Moreover, occurrences can be specified after every hypothesis after the {\TERM{at}} keyword. {\em concl} is either empty or \TERM{*}, and can be followed -by occurences. +by occurrences. \begin{transbox} \TRANS{in Goal}{in |- *} |