diff options
author | Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
commit | 234f5479773d43a48e67c5c0ea361445c7fb6782 (patch) | |
tree | 0609f0aef4769561d3bee2049c5c973f40b20be3 /doc/tools/Translator.tex | |
parent | 32415df7e24d4d79a00fae95a5f619980b006c61 (diff) |
Correct some spelling errorsmaster
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
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} |