MAJ biblio

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9078 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 31 insertions, 27 deletions

diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 103249f6e..4a8bad429 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -100,26 +100,25 @@ Computer Architecture},
         YEAR               = {1992}
 }
 
-@inproceedings{Bou97,
-   title = {Using reflection to build efficient and certified decision procedure
+@INPROCEEDINGS{Bou97,
+   TITLE       = {Using reflection to build efficient and certified decision procedure
 s},
-   author = {S. Boutin},
-   booktitle = {TACS'97},
-   editor = {Martin Abadi and Takahashi Ito},
-   publisher = SV,
-   series = lncs,
-   volume=1281, 
-   PS={http://pauillac.inria.fr/~boutin/public_w/submitTACS97.ps.gz}, 
-   year = {1997}
+   AUTHOR      = {S. Boutin},
+   BOOKTITLE   = {TACS'97},
+   EDITOR      = {Martin Abadi and Takahashi Ito},
+   PUBLISHER   = SV,
+   SERIES      = lncs,
+   VOLUME      = 1281, 
+   YEAR        = {1997}
 }
 
-@PhdThesis{Bou97These,
-  author =       {S. Boutin},
-  title =        {R\'eflexions sur les quotients},
-  school =       {Paris 7},
-  year =         1997,
-  type =         {th\`ese d'Universit\'e},
-  month =        apr
+@PHDTHESIS{Bou97These,
+  AUTHOR       = {S. Boutin},
+  TITLE        = {R\'eflexions sur les quotients},
+  SCHOOL       = {Paris 7},
+  YEAR         = 1997,
+  TYPE         = {th\`ese d'Universit\'e},
+  MONTH        = apr
 }
 
 @ARTICLE{Bru72,
@@ -525,14 +524,23 @@ s},
         YEAR               = {1994}
 }
 
-@TechReport{Gim98,
-  author = 	 {E. Gim\'enez},
-  title = 	 {A Tutorial on Recursive Types in Coq},
-  institution =  {INRIA},
-  year = 	 1998,
-  month =	 mar
+@TECHREPORT{Gim98,
+  AUTHOR       = {E. Gim\'enez},
+  TITLE        = {A Tutorial on Recursive Types in Coq},
+  INSTITUTION  = {INRIA},
+  YEAR         = 1998,
+  MONTH        = mar
 }
 
+@UNPUBLISHED{GimCas05,
+  AUTHOR       = {E. Gim\'enez and P. Cast\'eran},
+  TITLE        = {A Tutorial on [Co-]Inductive Types in Coq},
+  INSTITUTION  = {INRIA},
+  YEAR         = 2005,
+  MONTH        = jan,
+  NOTE         = {available at \url{http://coq.inria.fr/doc}}
+} 
+
 @INPROCEEDINGS{Gimenez95b,
         AUTHOR             = {E. Gim\'enez},
         BOOKTITLE          = {Workshop on Types for Proofs and Programs},
@@ -607,8 +615,6 @@ s},
         YEAR               = {1980}
 }
 
-
-
 @InProceedings{Hue87tapsoft,
   author = 	 {G. Huet},
   title = 	 {Programming of Future Generation Computers},
@@ -630,8 +636,6 @@ s},
         YEAR               = {1988}
 }
 
-
-
 @INPROCEEDINGS{Hue88,
         AUTHOR             = {G. Huet},
         BOOKTITLE          = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},