Fixing typos - Part 1

3 files changed, 6 insertions, 6 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}
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index 1de9890992..ba58ff0084 100644
--- a/doc/tools/coqrst/coqdoc/main.py
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -52,7 +52,7 @@ def is_whitespace_string(elem):
     return isinstance(elem, NavigableString) and elem.strip() == ""
 
 def strip_soup(soup, pred):
-    """Strip elements maching pred from front and tail of soup."""
+    """Strip elements matching pred from front and tail of soup."""
     while soup.contents and pred(soup.contents[-1]):
         soup.contents.pop()
 
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index 26f6255069..2b124ee5c1 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -47,7 +47,7 @@ class CoqTop:
         :param coqtop_bin: The path to coqtop; uses $COQBIN by default, falling back to "coqtop"
         :param color:      When True, tell coqtop to produce ANSI color codes (see
                            the ansicolors module)
-        :param args:       Additional arugments to coqtop.
+        :param args:       Additional arguments to coqtop.
         """
         self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop")
         if not pexpect.utils.which(self.coqtop_bin):
@@ -68,7 +68,7 @@ class CoqTop:
         self.coqtop.kill(9)
 
     def next_prompt(self):
-        """Wait for the next coqtop prompt, and return the output preceeding it."""
+        """Wait for the next coqtop prompt, and return the output preceding it."""
         self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10)
         return self.coqtop.before