1 files changed, 55 insertions, 0 deletions
diff --git a/doc/RecTutorial/morebib.bib b/doc/RecTutorial/morebib.bib
new file mode 100644
index 00000000..11dde2cd
--- /dev/null
+++ b/doc/RecTutorial/morebib.bib
@@ -0,0 +1,55 @@
+@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
+}
+
+@Article{Coquand:Huet,
+  author = 	 {Thierry Coquand and Gérard Huet},
+  title = 	 {The Calculus of Constructions},
+  journal = 	 {Information and Computation},
+  year = 	 {1988},
+  volume = 	 {76},
+}
+
+@INcollection{Coquand:metamathematical,
+ author = "Thierry Coquand",
+ title = "Metamathematical Investigations on a Calculus of Constructions",
+ booktitle="Logic and Computer Science",
+ year = {1990},
+ editor="P. Odifreddi",
+ publisher = "Academic Press",
+}
+
+@Misc{coqrefman,
+  title = {The {C}oq reference manual},
+  author={{C}oq {D}evelopment Team},
+  note= {LogiCal Project, \texttt{http://coq.inria.fr/}}
+ }
+
+@Misc{coqsite,
+  author= {{C}oq {D}evelopment Team},
+  title = 	 {The \emph{Coq} proof assistant},
+  note = {Documentation, system download. {C}ontact: \texttt{http://coq.inria.fr/}}
+}
+
+
+
+@Misc{Booksite,
+  author =	 {Yves Bertot and Pierre Cast\'eran},
+  title =	 {Coq'{A}rt: examples and exercises},
+  note =	 {\url{http://www.labri.fr/Perso/~casteran/CoqArt}}
+}
+
+
+@InProceedings{conor:motive,
+  author         ="Conor McBride",
+  title          = "Elimination with a motive",
+  booktitle =    "Types for Proofs and Programs'2000",
+  volume =         2277,
+  pages  =         "197-217",
+  year   =         "2002",
+}