aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/biblio.bib
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/biblio.bib')
-rw-r--r--doc/refman/biblio.bib15
1 files changed, 8 insertions, 7 deletions
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index b9a3a2c55..103249f6e 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1115,15 +1115,16 @@ Decomposition}},
note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
}
+@Book{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
+ }
-@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},