diff options
Diffstat (limited to 'doc/tools/Translator.tex')
| -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 3ee65d6f2..d8ac640f2 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} |