From 2d9566b5cc2c8bedc544cd6add8f000c8cc5013c Mon Sep 17 00:00:00 2001
From: mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 14 Dec 2003 22:18:08 +0000
Subject: Ajout these Bruno

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8394 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/biblio.bib | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/doc/biblio.bib b/doc/biblio.bib
index 96cf10028..8f38d2b60 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -1,4 +1,3 @@
-
 @string{jfp = "Journal of Functional Programming"}
 @STRING{lncs="Lecture Notes in Computer Science"}
 @STRING{lnai="Lecture Notes in Artificial Intelligence"}
@@ -990,6 +989,14 @@ Automated Reasoning},
         YEAR               = {1994}
 }
 
+@PHDTHESIS{Bar99,
+        AUTHOR             = {B. Barras},
+        SCHOOL             = {Universit\'e Paris 7},
+        TITLE              = {Auto-validation d'un système de preuves avec familles inductives,
+        TYPE               = {Th\`ese de Doctorat},
+        YEAR               = {1999}
+}
+
 @UNPUBLISHED{ddr98,
 	AUTHOR	           = {D. de Rauglaudre},
         TITLE              = {Camlp4 version 1.07.2},
@@ -1061,13 +1068,22 @@ Decomposition}},
 }
 
 
-
 @Misc{ProofGeneral,
   author =	 {David Aspinall},
   title =	 {Proof General},
   note =	 {\url{http://proofgeneral.inf.ed.ac.uk/}}
 }
 
+
+
+@Book{CoqArt,
+  author =	 {Yves bertot and Pierre Castéran},
+  title = 	 {Coq'Art},
+  publisher = 	 {Springer-Verlag},
+  year = 	 2004,
+  note =	 {To appear}
+}
+
 @INCOLLECTION{wadler87,
         AUTHOR             = {P. Wadler},
         TITLE              = {Efficient  Compilation of Pattern Matching},
-- 
cgit v1.2.3