CLEANUP PROPOSITION: Duplicate information was removed and replaced with a reference to the corresponding chapter.

1 files changed, 3 insertions, 36 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 7986648fb9..c481b3adba 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -5,42 +5,9 @@
 \index{Calculus of Inductive Constructions}}
 
 The underlying formal language of {\Coq} is a {\em Calculus of
-  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}).
-
-The reader seeking a background on the Calculus of Inductive
-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
-description of the \CIC{} based on numerous practical examples.
-Barras~\cite{Bar99}, Werner~\cite{Wer94} and
-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.
+Inductive Constructions} (\CIC) whose inference rules are presented in
+this chapter. The history of this formalism as well as pointers to related work
+are provided in a separate chapter; see {\em Credits}.
 
 \section[The terms]{The terms\label{Terms}}