From 935aa399ce4f26890f601d207d1cfee46b9ff6f3 Mon Sep 17 00:00:00 2001
From: kirchner
Date: Wed, 12 May 2004 12:54:27 +0000
Subject: MAJ bibtex Coq'Art

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8575 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/newfaq/fk.bib | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'doc')

diff --git a/doc/newfaq/fk.bib b/doc/newfaq/fk.bib
index c45e2c4ac4..5fd598fa93 100644
--- a/doc/newfaq/fk.bib
+++ b/doc/newfaq/fk.bib
@@ -106,13 +106,16 @@ year = {1981}
 
 %%%%%%% Coq %%%%%%%
 
-
-@unpublished{Coq:coqart,
-	author = "Y. Bertot and P. Casteran",
-	title = "{Le Coq'Art}",
-	url = "/Labri/Publications/Articles/coqart.ps.gz",
-}
-
+@book{Coq:coqart,
+  title = "Interactive Theorem Proving and Program Development,
+	  Coq'Art: The Calculus of Inductive Constructions",
+  author = "Yves Bertot and Pierre Castéran",
+  publisher = "Springer Verlag",
+  series = "Texts in Theoretical Computer Science. An
+	  EATCS series",
+  year = 2004
+}
+			 
 @phdthesis{Coq:Del01,
 	AUTHOR = "David Delahaye",
 	TITLE = "Conception de langages pour décrire les preuves et les 
-- 
cgit v1.2.3