RefMan, ch. 4: Reformulating introduction of the chapter on CIC, being

clearer that the version depends on the version of Coq.

Also renouncing to the "Predicative" and "(Co)" in the name, since
after all, usage seems to continue calling the language of Coq
Calculus of Inductive Constructions and to consider the Set
predicative vs Set impredicative, as well as the presence of
coinduction, as flavors of the CIC.

3 files changed, 57 insertions, 36 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 0e820008e..573c3c812 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -97,8 +97,7 @@
 \newcommand{\camlpppp}{\textsc{Camlp4}}
 \newcommand{\emacs}{\textsc{GNU Emacs}}
 \newcommand{\ProofGeneral}{\textsc{Proof General}}
-\newcommand{\CIC}{\pCIC}
-\newcommand{\pCIC}{p\textsc{Cic}}
+\newcommand{\CIC}{\textsc{Cic}}
 \newcommand{\iCIC}{\textsc{Cic}}
 \newcommand{\FW}{\ensuremath{F_{\omega}}}
 \newcommand{\Program}{\textsc{Program}}
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 2bf5bb357..a06e7acba 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -5,22 +5,29 @@
 \index{Calculus of Inductive Constructions}}
 
 The underlying formal language of {\Coq} is a {\em Calculus of
-  Constructions} with {\em Inductive Definitions}, also featuring a
-universe hierarchy and coinductive types. Its inference rules are
-presented in this chapter.
-
-For {\Coq} version V7, this Calculus was known as the
-{\em Calculus of Inductive Constructions}\index{Calculus of
-  Inductive Constructions} (\iCIC\ in short).
-The underlying calculus of {\Coq} version V8.0 and up is a weaker
-  calculus where the sort \Set{} satisfies predicative rules. 
-We call this calculus the 
-{\em Predicative Calculus of Inductive
-  Constructions}\index{Predicative Calculus of
-  Inductive Constructions} (\pCIC\ in short).
-In Section~\ref{impredicativity} we give the extra-rules for \iCIC. A
-  compiling option of \Coq{} allows type-checking theories in this
-  extended system.
+  Inductive Constructions} (\CIC) whose inference rules are presented in
+this chapter.
+
+The {\CIC} implemented in {\Coq}
+takes its name from Coquand and Paulin's {\em Calculus of
+  Inductive Constructions}~\cite{CoPa89} which itself extends
+Coquand-Huet's {\em Calculus of
+  Constructions}~\cite{CoHu85a,CoHu85b,CoHu86,Coq85} with a universe
+hierarchy~\cite{Coq86,Luo90,Hue88b} and a generic presentation of
+inductive types à la Martin-L\"of~\cite{MaL84,Dyb91}. First implemented in
+{\Coq} version 5.0, it incorporated coinductive
+types~\cite{Coquand93,Gim96} from {\Coq} version 5.10. It
+progressively extended with various new features such as local
+definitions (since {\Coq} version 7.0), universe polymorphism (since
+{\Coq} version 8.1 for inductive types and version 8.5 for full
+polymorphism), recursively non-uniform parameters (since {\Coq} version 8.1),
+some $\eta$-rules (for dependent product in {\Coq}
+version 8.4, for record types in {\Coq} version 8.5), and other
+refinements in the expressiveness of fixpoints and inductive types.
+Up to version 7.4, the {\CIC} implemented in {\Coq}
+had an impredicative sort {\Set}. Since {\Coq} version 8.0, the sort
+{\Set} is predicative by default, with an option to make it
+impredicative (see Section~\ref{impredicativity}).
 
 In \CIC\, all objects have a {\em type}. There are types for functions (or
 programs), there are atomic types (especially datatypes)... but also
@@ -28,29 +35,25 @@ types for proofs and types for the types themselves.
 Especially, any object handled in the formalism must belong to a
 type.  For instance, the statement {\it ``for all x, P''} is not
 allowed in type theory; you must say instead: {\it ``for all x
-belonging to T, P''}. The expression {\it ``x belonging to T''} is
-written {\it ``x:T''}. One also says: {\it ``x has type T''}.
+of type T, P''}. The expression {\it ``x of type T''} is
+written {\it ``x:T''}. Informally, {\it ``x:T''} can be thought as
+{\it ``x belongs to T''}.
 The terms of {\CIC} are detailed in Section~\ref{Terms}.
 
-In \CIC\, there is an internal reduction mechanism. In particular, it
+In \CIC, there is an internal reduction mechanism. In particular, it
 can decide if two programs are {\em intentionally} equal (one
 says {\em convertible}). Convertibility is presented in section 
 \ref{convertibility}.
 
-The remaining sections are concerned with the type-checking of terms.
-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}
+Constructions may read several papers. In addition to the references given above, Giménez and Castéran~\cite{GimCas05}
 provide
 an introduction to inductive and co-inductive definitions in Coq. In
-their book~\cite{CoqArt}, Bertot and Castéran give a precise
+their book~\cite{CoqArt}, Bertot and Castéran give a
 description of the \CIC{} based on numerous practical examples.
 Barras~\cite{Bar99}, Werner~\cite{Wer94} and
-Paulin-Mohring~\cite{Moh97} are the most recent theses dealing with
-Inductive Definitions. Coquand-Huet~\cite{CoHu85a,CoHu85b,CoHu86}
-introduces the Calculus of Constructions. Coquand-Paulin~\cite{CoPa89}
-extended this calculus to inductive definitions. The {\CIC} is a
+Paulin-Mohring~\cite{Moh97} are dealing with
+Inductive Definitions. The {\CIC} is a
 formulation of type theory including the possibility of inductive
 constructions, Barendregt~\cite{Bar91} studies the modern form of type
 theory.
@@ -1701,11 +1704,11 @@ More information on co-inductive definitions can be found
 in~\cite{Gimenez95b,Gim98,GimCas05}.
 %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
+\section[The Calculus of Inductive Construction with
+  impredicative \Set]{The Calculus of Inductive Construction with
   impredicative \Set\label{impredicativity}}
 
-\Coq{} can be used as a type-checker for \iCIC{}, the original 
+\Coq{} can be used as a type-checker for the
 Calculus of Inductive Constructions with an impredicative sort \Set{}
 by using the compiler option \texttt{-impredicative-set}.
 
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index d78ce4f2c..6f789b081 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -288,9 +288,14 @@ s},
 
 @InProceedings{Coquand93,
   author      = {Th. Coquand},
-  title       = {{Infinite Objects in Type Theory}},
+  booktitle   = {Types for Proofs and Programs},
+  editor      = {H. Barendregt and T. Nipokow},
+  publisher   = SV,
+  series      = LNCS,
+  title       = {{Infinite objects in Type Theory}},
+  volume      = {806},
   year        = {1993},
-  crossref    = {Nijmegen93}
+  pages       = {62-78}
 }
 
 @inproceedings{Corbineau08types,
@@ -540,6 +545,13 @@ s},
   year        = {1994}
 }
 
+@PhDThesis{Gim96,
+  author      = {E. Gim\'enez},
+  title       = {Un calcul des constructions infinies et son application \'a la v\'erification de syst\`emes communicants},
+  school      = {\'Ecole Normale Sup\'erieure de Lyon},
+  year        = {1996}
+}
+
 @TechReport{Gim98,
   author      = {E. Gim\'enez},
   title       = {A Tutorial on Recursive Types in Coq},
@@ -660,6 +672,13 @@ s},
   year        = {1989}
 }
 
+@Unpublished{Hue88b,
+  author      = {G. Huet},
+  title       = {Extending the Calculus of Constructions with Type:Type},
+  year        = 1988,
+  note        = {Unpublished}
+}
+
 @Book{Hue89,
   editor      = {G. Huet},
   publisher   = {Addison-Wesley},
@@ -1366,4 +1385,4 @@ Languages},
   timestamp = {Thu, 17 Nov 2011 13:33:48 +0100},
   biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11},
   bibsource = {dblp computer science bibliography, http://dblp.org}
-}
\ No newline at end of file
+}