1 files changed, 0 insertions, 55 deletions
diff --git a/doc/RecTutorial/morebib.bib b/doc/RecTutorial/morebib.bib
deleted file mode 100644
index 11dde2cd..00000000
--- a/doc/RecTutorial/morebib.bib
+++ /dev/null
@@ -1,55 +0,0 @@
-@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",
-}