diff options
| author | herbelin | 2006-08-24 08:47:46 +0000 |
|---|---|---|
| committer | herbelin | 2006-08-24 08:47:46 +0000 |
| commit | 90d7d595fd0b46f4c9766b747bd7f57428376e12 (patch) | |
| tree | fda84955950af2ca1ce6ea082c25fa032107c5f9 | |
| parent | 3c20af573b22e470589e8d19e91a798b3fdbc917 (diff) | |
MAJ biblio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9080 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |