1 files changed, 25 insertions, 0 deletions
diff --git a/doc/biblio.bib b/doc/biblio.bib
index 2e97d1e071..653944c9d3 100755
--- a/doc/biblio.bib
+++ b/doc/biblio.bib
@@ -618,6 +618,21 @@ 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},
@@ -776,6 +791,16 @@ the Calculus of Inductive Constructions}},
         YEAR               = {1993}
 }
 
+@BOOK{RC95,
+  author = "di~Cosmo, R.",
+  title  = "Isomorphisms of Types: from $\lambda$-calculus to information
+            retrieval and language design",
+  series = "Progress in Theoretical Computer Science",
+  publisher = "Birkhauser",
+  year = "1995",
+  note = "ISBN-0-8176-3763-X"
+}
+
 @TECHREPORT{Rou92,
         AUTHOR             = {J. Rouyer},
         INSTITUTION        = {INRIA},