From 45a4f91f3a8e616f870801be506e46c15d284a04 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 19 Dec 2003 22:25:08 +0000
Subject: Typos

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8427 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-modr.tex | 6 +++---
 doc/RefMan-pre.tex  | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/doc/RefMan-modr.tex b/doc/RefMan-modr.tex
index c5f3097635..f9a251fdc9 100644
--- a/doc/RefMan-modr.tex
+++ b/doc/RefMan-modr.tex
@@ -2,7 +2,7 @@
 \label{Mod}
 
 The module system extends the Calculus of Inductive Constructions
-providing a convinient way to structure large developments as well as
+providing a convenient way to structure large developments as well as
 a mean of massive abstraction.
 %It is described in details in Judicael's thesis and Jacek's thesis
 
@@ -56,7 +56,7 @@ $S$ is a module type name and $T$ is a module type.
 In order to introduce the typing system we first slightly extend
 the syntactic class of terms and environments given in
 section~\ref{Terms}. The environments, apart from definitions of
-constants and inductives now also hold any other signature elements.
+constants and inductive types now also hold any other signature elements.
 Terms, apart from variables, constants and complex terms, 
 include also access paths.
 
@@ -146,7 +146,7 @@ Rules for typing module expressions:
   }
 }
 \end{itemize}
-The last rule, called strengthenning is used to make all module fields
+The last rule, called strengthening is used to make all module fields
 manifestly equal to themselves. The notation $T/p$ has the following
 meaning:
 \begin{itemize}
diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index a36148741e..2e53af5982 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -429,7 +429,7 @@ revised. The main motivations were
 \item lighter expressions: the ``(id:t)u'' notation for products
   was forbidding the omission of the types. This is now
   possible. Also, parentheses are no longer mandatory for function
-  application. The choice here was to follow the tested style of
+  application. The choice here was to follow the long-standing style of
   syntax found in typed functional programming (which is compatible
   with polymorphism) rather than the mathematical style (which 
   harmonizes badly with polymorphism).
@@ -452,7 +452,7 @@ of {\Coq} has been performed. There is now just one Leibniz' equality
 usable for all the different kinds of {\Coq} objects. Also, the set of
 real numbers now lies at the same level as the sets of natural and
 integer numbers. Finally, the names of the standard properties of
-numbers now follow a standard scheme pattern and the symbolic
+numbers now follow a standard pattern and the symbolic
 notations for the standard definitions as well.
 
 The fourth point is the release of \CoqIde{}, a new graphical
@@ -492,7 +492,7 @@ Benjamin Monate is the developer of the \CoqIde{} graphical
 interface with contributions by Jean-Christophe Filliâtre, Pierre
 Letouzey and Claude Marché.
 
-Claude Marché coordinated the edition od the Reference Manual for
+Claude Marché coordinated the edition of the Reference Manual for
  \Coq{} V8.0.
 
 Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the
-- 
cgit v1.2.3