Mise-a-jour de la biblio

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

2 files changed, 26 insertions, 22 deletions

diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index bc79cbbe81..9ad394e5f6 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -10,7 +10,7 @@ This chapter gives a compact documentation of the tactic language available in
 the toplevel of {\Coq}. We start by giving the syntax and, next, we present the
 informal semantic. Finally, we show some examples which deal with small but
 also with non-trivial problems. If you want to know more regarding this
-language and especially about its fundations, you can refer to~\cite{LTAC}.
+language and especially about its fundations, you can refer to~\cite{Del00}.
 
 \section{Syntax}
 
diff --git a/doc/biblio.bib b/doc/biblio.bib
index ad0ff37c0f..18630fe4ef 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -284,12 +284,31 @@ s},
         YEAR               = {1994}
 }
 
-@MASTERSTHESIS{Del97,
-        AUTHOR             = {D. Delahaye},
-        MONTH              = sep,
-        SCHOOL             = {DEA S{\'e}mantique, Preuves et Programmation, Paris 6},
-        TITLE              = {Search2: un outil de recherche dans une biblioth\`eque de preuves Coq modulo isomorphismes},
-        YEAR               = {1997}
+@INPROCEEDINGS{Del99,
+  author    = "Delahaye, D.",
+  title     = "Information {R}etrieval in a {{\sf Coq}} {P}roof {L}ibrary using
+               {T}ype {I}somorphisms",
+  booktitle = "Proceedings of TYPES'99, Lökeberg",
+  publisher = "Springer-Verlag LNCS",
+  year      = "1999",
+  note      =
+    "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
+    "{\sf TYPES99-SIsos.ps.gz}"
+}
+
+@INPROCEEDINGS{Del00,
+  author    = "Delahaye, D.",
+  title     = "A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}",
+  booktitle = "Proceedings of Logic for Programming and Automated Reasoning
+               (LPAR), Reunion Island",
+  publisher = "Springer-Verlag LNCS/LNAI",
+  volume    = "1955",
+  pages     = "85--95",
+  month     = "November",
+  year      = "2000",
+  note      =
+    "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
+    "{\sf LPAR2000-ltac.ps.gz}"
 }
 
 @INPROCEEDINGS{DelMay01,
@@ -678,21 +697,6 @@ of the {ML} language},
         YEAR               = {1990}
 }
 
-@INPROCEEDINGS{LTAC,
-  author    = "Delahaye, D.",
-  title     = "A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}",
-  booktitle = "Proceedings of Logic for Programming and Automated Reasoning
-               (LPAR), Reunion Island",
-  publisher = "Springer-Verlag LNCS/LNAI",
-  volume    = "1955",
-  pages     = "85--95",
-  month     = "November",
-  year      = "2000",
-  note      =
-    "{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"#
-    "{\sf LPAR2000-ltac.ps.gz}"
-}
-
 @BOOK{MaL84,
         AUTHOR             = {{P. Martin-L\"of}},
         PUBLISHER          = {Bibliopolis},