diff options
| -rw-r--r-- | doc/RefMan-modr.tex | 6 | ||||
| -rwxr-xr-x | 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 c5f309763..f9a251fdc 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 a36148741..2e53af598 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 |