Pr�noms

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

1 files changed, 30 insertions, 30 deletions

diff --git a/doc/newfaq/fk.bib b/doc/newfaq/fk.bib
index 5fd598fa93..392e401fc8 100644
--- a/doc/newfaq/fk.bib
+++ b/doc/newfaq/fk.bib
@@ -1,7 +1,7 @@
 %%%%%%% FAQ %%%%%%%
 
 @book{ProofsTypes,
-  Author="Girard, J.-Y. and Y. Lafont and P. Taylor",
+  Author="Girard, Jean-Yves and Yves Lafont and Paul Taylor",
   Title="Proofs and Types",
   Publisher="Cambrige Tracts in Theoretical Computer Science, Cambridge University Press",
   Year="1989"
@@ -16,7 +16,7 @@
 }
 
 @PHDTHESIS{EGThese,
-  author = {E. Giménez},
+  author = {Eduardo Giménez},
   title = {Un Calcul de Constructions Infinies et son application
 a la vérification de systèmes communicants},
   type = {thèse d'Université},
@@ -126,7 +126,7 @@ year = {1981}
 }
 
 @techreport{Coq:gimenez-tut,
-    author = "Eduardo Gimenez",
+    author = "Eduardo Gim\'enez",
     title = "A Tutorial on Recursive Types in Coq",
     number = "RT-0221",
     pages = "42 p.",
@@ -153,7 +153,7 @@ year = {1981}
 }
 
 @manual{Coq:Tutorial,
-  AUTHOR = {G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring},
+  AUTHOR = {G\'erard Huet and Gilles Kahn and Christine Paulin-Mohring},
   TITLE = {{The Coq Proof Assistant A Tutorial}},
   YEAR = 2004  
 }
@@ -426,7 +426,7 @@ nd Applications},
 }
 
 @PHDTHESIS{Pau96b,
-  AUTHOR = {C. Paulin-Mohring},
+  AUTHOR = {Christine Paulin-Mohring},
   TITLE = {Définitions Inductives en Théorie des Types d'Ordre Supérieur},
   SCHOOL = {Université Claude Bernard Lyon I},
   YEAR = 1996,
@@ -1060,7 +1060,7 @@ and Erik Poll and Nicole Rauch and Xavier Urbain},
         publisher       = "Springer-Verlag"}
 
 @InCollection{howe,
-  author =       {D. Howe},
+  author =       {Doug Howe},
   title =        {Computation Meta theory in Nuprl},
   booktitle =    {The Proceedings of the Ninth International Conference of Autom
 ated Deduction},
@@ -1072,7 +1072,7 @@ ated Deduction},
 }
 
 @TechReport{harrison,
-  author =       {J. Harrison},
+  author =       {John Harrison},
   title =        {Meta theory and Reflection in Theorem Proving:a Survey and Cri
 tique},
   institution =  {SRI International Cambridge Computer Science Research Center},
@@ -1081,7 +1081,7 @@ tique},
 }
 
 @InCollection{cc,
-  author =       {Th. Coquand and G. Huet},
+  author =       {Thierry Coquand and Gérard Huet},
   title =        {The Calculus of Constructions},
   booktitle =    {Information and Computation},
   year =         {1988},
@@ -1091,7 +1091,7 @@ tique},
 
 
 @InProceedings{coquandcci,
-  author =       {Th. Coquand and C. Paulin-Mohring},
+  author =       {Thierry Coquand and Christine Paulin-Mohring},
   title =        {Inductively defined types},
   booktitle =    {Proceedings of Colog'88},
   year =         {1990},
@@ -1103,7 +1103,7 @@ tique},
 
 
 @InProceedings{boutin,
-  author =       {S. Boutin},
+  author =       {Samuel Boutin},
   title =        {Using reflection to build efficient and certified decision pro
 cedures.},
   booktitle =    {Proceedings of TACS'97},
@@ -1318,7 +1318,7 @@ s},
 }
 
 @INPROCEEDINGS{CoHu85a,
-        AUTHOR             = {Th. Coquand and G. Huet},
+        AUTHOR             = {Thierry Coquand and Gérard Huet},
         ADDRESS            = {Linz},
         BOOKTITLE          = {EUROCAL'85},
         PUBLISHER          = SV,
@@ -1329,7 +1329,7 @@ s},
 }
 
 @INPROCEEDINGS{CoHu85b,
-        AUTHOR             = {Th. Coquand and G. Huet},
+        AUTHOR             = {Thierry Coquand and Gérard Huet},
         BOOKTITLE          = {Logic Colloquium'85},
         EDITOR             = {The Paris Logic Group},
         PUBLISHER          = {North-Holland},
@@ -1338,7 +1338,7 @@ s},
 }
 
 @ARTICLE{CoHu86,
-        AUTHOR             = {Th. Coquand and G. Huet},
+        AUTHOR             = {Thierry Coquand and Gérard Huet},
         JOURNAL            = {Information and Computation},
         NUMBER             = {2/3},
         TITLE              = {The {Calculus of Constructions}},
@@ -1347,7 +1347,7 @@ s},
 }
 
 @INPROCEEDINGS{CoPa89,
-        AUTHOR             = {Th. Coquand and C. Paulin-Mohring},
+        AUTHOR             = {Thierry Coquand and Christine Paulin-Mohring},
         BOOKTITLE          = {Proceedings of Colog'88},
         EDITOR             = {P. Martin-L\"of and G. Mints},
         PUBLISHER          = SV,
@@ -1365,7 +1365,7 @@ s},
 }
 
 @PHDTHESIS{Coq85,
-        AUTHOR             = {Th. Coquand},
+        AUTHOR             = {Thierry Coquand},
         MONTH              = jan,
         SCHOOL             = {Universit\'e Paris~7},
         TITLE              = {Une Th\'eorie des Constructions},
@@ -1373,7 +1373,7 @@ s},
 }
 
 @INPROCEEDINGS{Coq86,
-        AUTHOR             = {Th. Coquand},
+        AUTHOR             = {Thierry Coquand},
         ADDRESS            = {Cambridge, MA},
         BOOKTITLE          = {Symposium on Logic in Computer Science},
         PUBLISHER          = {IEEE Computer Society Press},
@@ -1382,7 +1382,7 @@ s},
 }
 
 @INPROCEEDINGS{Coq90,
-        AUTHOR             = {Th. Coquand},
+        AUTHOR             = {Thierry Coquand},
         BOOKTITLE          = {Logic and Computer Science},
         EDITOR             = {P. Oddifredi},
         NOTE               = {INRIA Research Report 1088, also in~\cite{CoC89}},
@@ -1392,7 +1392,7 @@ s},
 }
 
 @INPROCEEDINGS{Coq91,
-        AUTHOR             = {Th. Coquand},
+        AUTHOR             = {Thierry Coquand},
         BOOKTITLE          = {Proceedings 9th Int. Congress of Logic, Methodology and Philosophy of Science},
         TITLE              = {{A New Paradox in Type Theory}},
         MONTH              = {August},
@@ -1400,14 +1400,14 @@ s},
 }
 
 @INPROCEEDINGS{Coq92,
-        AUTHOR             = {Th. Coquand},
+        AUTHOR             = {Thierry Coquand},
         TITLE              = {{Pattern Matching with Dependent Types}},
         YEAR               = {1992},
         crossref = {Bastad92}
 }
 
 @INPROCEEDINGS{Coquand93,
-        AUTHOR             = {Th. Coquand},
+        AUTHOR             = {Thierry Coquand},
         TITLE              = {{Infinite Objects in Type Theory}},
         YEAR               = {1993},
         crossref = {Nijmegen93}
@@ -1631,7 +1631,7 @@ s},
 }
 
 @INPROCEEDINGS{Gim94,
-        AUTHOR             = {E. Gim\'enez},
+        AUTHOR             = {Eduardo Gim\'enez},
         BOOKTITLE          = {Types'94 : Types for Proofs and Programs},
         NOTE               = {Extended version in LIP research report 95-07, ENS Lyon},
         PUBLISHER          = SV,
@@ -1663,7 +1663,7 @@ s},
 }
 
 @INPROCEEDINGS{Gir70,
-        AUTHOR             = {J.-Y. Girard},
+        AUTHOR             = {Jean-Yves Girard},
         BOOKTITLE          = {Proceedings of the 2nd Scandinavian Logic Symposium},
         PUBLISHER          = {North-Holland},
         TITLE              = {Une extension de l'interpr\'etation de {G\"odel} \`a l'analyse, et son application \`a l'\'elimination des coupures dans l'analyse et la th\'eorie des types},
@@ -1671,7 +1671,7 @@ s},
 }
 
 @PHDTHESIS{Gir72,
-        AUTHOR             = {J.-Y. Girard},
+        AUTHOR             = {Jean-Yves Girard},
         SCHOOL             = {Universit\'e Paris~7},
         TITLE              = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur},
         YEAR               = {1972}
@@ -1680,7 +1680,7 @@ s},
 
 
 @BOOK{Gir89,
-        AUTHOR             = {J.-Y. Girard and Y. Lafont and P. Taylor},
+        AUTHOR             = {Jean-Yves Girard and Yves Lafont and Paul Taylor},
         PUBLISHER          = {Cambridge University Press},
         SERIES             = {Cambridge Tracts in Theoretical Computer Science 7},
         TITLE              = {Proofs and Types},
@@ -1698,7 +1698,7 @@ s},
 }
 
 @MASTERSTHESIS{Hir94,
-        AUTHOR             = {D. Hirschkoff},
+        AUTHOR             = {Daniel Hirschkoff},
         MONTH              = sep,
         SCHOOL             = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
         TITLE              = {{\'E}criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
@@ -1893,7 +1893,7 @@ of the {ML} language},
 }
 
 @INPROCEEDINGS{Moh89a,
-        AUTHOR             = {C. Paulin-Mohring},
+        AUTHOR             = {Christine Paulin-Mohring},
         ADDRESS            = {Austin},
         BOOKTITLE          = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
         MONTH              = jan,
@@ -1903,7 +1903,7 @@ of the {ML} language},
 }
 
 @PHDTHESIS{Moh89b,
-        AUTHOR             = {C. Paulin-Mohring},
+        AUTHOR             = {Christine Paulin-Mohring},
         MONTH              = jan,
         SCHOOL             = {{Universit\'e Paris 7}},
         TITLE              = {Extraction de programmes dans le {Calcul des Constructions}},
@@ -1911,7 +1911,7 @@ of the {ML} language},
 }
 
 @INPROCEEDINGS{Moh93,
-        AUTHOR             = {C. Paulin-Mohring},
+        AUTHOR             = {Christine Paulin-Mohring},
         BOOKTITLE          = {Proceedings of the conference Typed Lambda Calculi and Applications},
         EDITOR             = {M. Bezem and J.-F. Groote},
         NOTE               = {Also LIP research report 92-49, ENS Lyon},
@@ -1923,7 +1923,7 @@ of the {ML} language},
 }
 
 @BOOK{Moh97,
-        AUTHOR             = {C. Paulin-Mohring},
+        AUTHOR             = {Christine Paulin-Mohring},
         MONTH              = jan,
         PUBLISHER          = {{ENS Lyon}},
         TITLE              = {{Le syst\`eme Coq. \mbox{Th\`ese d'habilitation}}},
@@ -1987,7 +1987,7 @@ of the {ML} language},
 }
 
 @ARTICLE{PaWe92,
-        AUTHOR             = {C. Paulin-Mohring and B. Werner},
+        AUTHOR             = {Christine Paulin-Mohring and Benjamin Werner},
         JOURNAL            = {Journal of Symbolic Computation},
         PAGES              = {607--640},
         TITLE              = {{Synthesis of ML programs in the system Coq}},