aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/newfaq/fk.bib17
1 files changed, 10 insertions, 7 deletions
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