Fix various typos in documentation

Closes #57.

5 files changed, 7 insertions, 7 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index e802398b55..76bcaaae67 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -5,7 +5,7 @@
 
 We present here the \Program\ tactic commands, used to build certified
 \Coq\ programs, elaborating them from their algorithmic skeleton and a
-rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction
+rich specification \cite{Sozeau06}. It can be thought of as a dual of extraction
 (see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular
 functional programming language whilst using as rich a specification as 
 desired and proving that the code meets the specification using the whole \Coq{} proof
@@ -48,7 +48,7 @@ operation (see Section~\ref{Caseexpr}).
   | S n => u
   end.
 \end{coq_example*}
-will be first rewrote to:
+will be first rewritten to:
 \begin{coq_example*}
   (match x as y return (x = y -> _) with
   | 0 => fun H : x = 0 -> t
@@ -108,7 +108,7 @@ goals to construct the final definitions.
 \subsection{\tt Program Definition {\ident} := {\term}.
   \comindex{Program Definition}\label{ProgramDefinition}}
 
-This command types the value {\term} in \Russell\ and generate proof
+This command types the value {\term} in \Russell\ and generates proof
 obligations. Once solved using the commands shown below, it binds the final
 \Coq\ term to the name {\ident} in the environment.
 
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 48b9315e37..e56c8fa7fe 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -3,7 +3,7 @@
 \label{section:Modules}}
 
 The module system provides a way of packaging related elements
-together, as well as a mean of massive abstraction.
+together, as well as a means of massive abstraction.
 
 \begin{figure}[t]
 \begin{centerframe}
diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex
index 9ab8aded9c..2019a529fe 100644
--- a/doc/refman/RefMan-modr.tex
+++ b/doc/refman/RefMan-modr.tex
@@ -2,7 +2,7 @@
 
 The module system extends the Calculus of Inductive Constructions
 providing a convenient way to structure large developments as well as
-a mean of massive abstraction.
+a means of massive abstraction.
 %It is described in details in Judicael's thesis and Jacek's thesis
 
 \section{Modules and module types}
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index b42480a569..ee2b042f4e 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -141,7 +141,7 @@ Example:
 \end{verbatim}
 
 \paragraph{Rules.}
-More than 4 leading dashes produce an horizontal rule.
+More than 4 leading dashes produce a horizontal rule.
 
 \paragraph{Emphasis.}
 Text can be italicized by placing it in underscores.  A non-identifier
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 424ca0c8cc..a7bdba90aa 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -59,7 +59,7 @@ Reserved Notation "( x , y , .. , z )" (at level 0).
 
 (** Notation "{ x }" is reserved and has a special status as component
     of other notations such as "{ A } + { B }" and "A + { B }" (which
-    are at the same level than "x + y");
+    are at the same level as "x + y");
     "{ x }" is at level 0 to factor with "{ x : A | P }" *)
 
 Reserved Notation "{ x }" (at level 0, x at level 99).