From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 doc/refman/RefMan-cic.tex | 77 +++++++++++++++++++++++++++--------------------
 1 file changed, 45 insertions(+), 32 deletions(-)

(limited to 'doc/refman/RefMan-cic.tex')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 9660a04b..6a132eba 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -41,7 +41,7 @@ The beginner can skip them.
 The reader seeking a background on the Calculus of Inductive
 Constructions may read several papers. Giménez and Castéran~\cite{GimCas05} 
 provide
-an introduction to inductive and coinductive definitions in Coq. In
+an introduction to inductive and co-inductive definitions in Coq. In
 their book~\cite{CoqArt}, Bertot and Castéran give a precise
 description of the \CIC{} based on numerous practical examples.
 Barras~\cite{Bar99}, Werner~\cite{Wer94} and
@@ -80,35 +80,48 @@ type $(P~n)$ and consequently represent proofs of the formula
 
 \subsection[Sorts]{Sorts\label{Sorts}
 \index{Sorts}}
-Types are seen as terms of the language and then should belong to
-another type. The type of a type is always a constant of the language
-called a {\em sort}.
-
-The two basic sorts in the language of \CIC\ are \Set\ and \Prop.
-
-The sort \Prop\ intends to be the type of logical propositions.  If
-$M$ is a logical proposition then it denotes a class, namely the class
-of terms representing proofs of $M$. An object $m$ belonging to $M$
-witnesses the fact that $M$ is true.  An object of type \Prop\ is
-called a {\em proposition}.
-
-The sort \Set\ intends to be the type of specifications. This includes
-programs and the usual sets such as booleans, naturals, lists
-etc.
-
-These sorts themselves can be manipulated as ordinary terms.
-Consequently sorts also should be given a type.  Because assuming
-simply that \Set\ has type \Set\ leads to an inconsistent theory, we
-have infinitely many sorts in the language of \CIC. These are, in
-addition to \Set\ and \Prop\, a hierarchy of universes \Type$(i)$
-for any integer $i$.  We call \Sort\ the set of sorts
-which is defined by:
+When manipulated as terms, types have themselves a type which is called a sort.
+
+There is an infinite well-founded typing hierarchy of sorts whose base
+sorts are {\Prop} and {\Set}.
+
+The sort {\Prop} intends to be the type of logical propositions. If
+$M$ is a logical proposition then it denotes the class of terms
+representing proofs of $M$. An object $m$ belonging to $M$ witnesses
+the fact that $M$ is provable. An object of type {\Prop} is called a
+proposition.
+
+The sort {\Set} intends to be the type of small sets. This includes data
+types such as booleans and naturals, but also products, subsets, and
+function types over these data types.
+
+{\Prop} and {\Set} themselves can be manipulated as ordinary
+terms. Consequently they also have a type. Because assuming simply
+that {\Set} has type {\Set} leads to an inconsistent theory, the
+language of {\CIC} has infinitely many sorts. There are, in addition
+to {\Set} and {\Prop} a hierarchy of universes {\Type$(i)$} for any
+integer $i$.
+
+Like {\Set}, all of the sorts {\Type$(i)$} contain small sets such as
+booleans, natural numbers, as well as products, subsets and function
+types over small sets. But, unlike {\Set}, they also contain large
+sets, namely the sorts {\Set} and {\Type$(j)$} for $j<i$, and all
+products, subsets and function types over these sorts.
+
+Formally, we call {\Sort} the set of sorts which is defined by:
 \[\Sort \equiv \{\Prop,\Set,\Type(i)| i \in \NN\} \]
 \index{Type@{\Type}}
 \index{Prop@{\Prop}}
 \index{Set@{\Set}}
-The sorts enjoy the following properties: {\Prop:\Type(0)}, {\Set:\Type(0)} and
-  {\Type$(i)$:\Type$(i+1)$}.
+
+The sorts enjoy the following properties\footnote{In the Reference
+  Manual of versions of Coq prior to 8.4, the level of {\Type} typing
+  {\Prop} and {\Set} was numbered $0$. From Coq 8.4, it started to be
+  numbered $1$ so as to be able to leave room for re-interpreting
+  {\Set} in the hierarchy as {\Type$(0)$}. This change also put the
+  reference manual in accordance with the internal conventions adopted
+  in the implementation.}: {\Prop:\Type$(1)$}, {\Set:\Type$(1)$} and
+{\Type$(i)$:\Type$(i+1)$}.
 
 The user will never mention explicitly the index $i$ when referring to
 the universe \Type$(i)$. One only writes \Type. The
@@ -420,9 +433,9 @@ convertibility into an order inductively defined by:
 \begin{enumerate}
 \item if $\WTEGCONV{t}{u}$ then $\WTEGLECONV{t}{u}$,
 \item if $i \leq j$ then $\WTEGLECONV{\Type(i)}{\Type(j)}$,
-\item for any $i$, $\WTEGLECONV{\Prop}{\Type(i)}$,
 \item for any $i$, $\WTEGLECONV{\Set}{\Type(i)}$,
-\item $\WTEGLECONV{\Prop}{\Set}$,
+\item $\WTEGLECONV{\Prop}{\Set}$, hence, by transitivity,
+  $\WTEGLECONV{\Prop}{\Type(i)}$, for any $i$
 \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T,T'}{\forall~x:U,U'}$.
 \end{enumerate}
 
@@ -1650,12 +1663,12 @@ Abort.
 The principles of mutual induction can be automatically generated 
 using the {\tt Scheme} command described in Section~\ref{Scheme}.
 
-\section{Coinductive types}
-The implementation contains also coinductive definitions, which are
+\section{Co-inductive types}
+The implementation contains also co-inductive definitions, which are
 types inhabited by infinite objects. 
-More information on coinductive definitions can be found
+More information on co-inductive definitions can be found
 in~\cite{Gimenez95b,Gim98,GimCas05}.
-%They are described in Chapter~\ref{Coinductives}.
+%They are described in Chapter~\ref{Co-inductives}.
 
 \section[\iCIC : the Calculus of Inductive Construction with
   impredicative \Set]{\iCIC : the Calculus of Inductive Construction with
-- 
cgit v1.2.3