Fixing typos - Part 1

1 files changed, 3 insertions, 3 deletions

diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index d8ac640f2a..dde8a7b838 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -412,7 +412,7 @@ but its behaviour is not to fold the abbreviation at all.}.
 {\tt LetTac} could be followed by a specification (called a clause) of
 the places where the abbreviation had to be folded (hypothese and/or
 conclusion). Clauses are the syntactic notion to denote in which parts
-of a goal a given transformation shold occur. Its basic notation is
+of a goal a given transformation should occur. Its basic notation is
 either \TERM{*} (meaning everywhere), or {\tt\textrm{\em hyps} |-
 \textrm{\em concl}} where {\em hyps} is either \TERM{*} (to denote all
 the hypotheses), or a comma-separated list of either hypothesis name,
@@ -620,7 +620,7 @@ These constraints are met by the makefiles produced by {\tt coq\_makefile}
 
 Otherwise, modify your build program so as to pass option {\tt
 -translate} to program {\tt coqc}. The effect of this option is to
-ouptut the translated source of any {\tt .v} file in a file with
+output the translated source of any {\tt .v} file in a file with
 extension {\tt .v8} located in the same directory than the original
 file.
 
@@ -675,7 +675,7 @@ solve all occurrences of the problem.
 The definition of identifiers changed. Most of those changes are
 handled by the translator. They include:
 \begin{itemize}
-\item {\tt \_} is not an identifier anymore: it is tranlated to {\tt
+\item {\tt \_} is not an identifier anymore: it is translated to {\tt
 x\_}
 \item avoid clash with new keywords by adding a trailing {\tt \_}
 \end{itemize}