diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 50fb7c08e2..a79f9d2b68 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -39,7 +39,8 @@ 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~\cite{Gim98} provides +Constructions may read several papers. Giménez and Castéran~\cite{GimCas05} +provide an introduction to inductive and coinductive definitions in Coq. In their book~\cite{CoqArt}, Bertot and Castéran give a precise description of the \CIC{} based on numerous practical examples. @@ -1633,7 +1634,7 @@ using the {\tt Scheme} command described in section~\ref{Scheme}. The implementation contains also coinductive definitions, which are types inhabited by infinite objects. More information on coinductive definitions can be found -in~\cite{Gimenez95b,Gim98}. +in~\cite{Gimenez95b,Gim98,GimCas05}. %They are described in chapter~\ref{Coinductives}. \section{\iCIC : the Calculus of Inductive Construction with |