*** empty log message ***

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

2 files changed, 32 insertions, 31 deletions

diff --git a/doc/newfaq/fk.bib b/doc/newfaq/fk.bib
index d52cac0a6..77baf9799 100644
--- a/doc/newfaq/fk.bib
+++ b/doc/newfaq/fk.bib
@@ -1,30 +1,31 @@
-%%%%%%% F %%%%%%%
+%%%%%%% FAQ %%%%%%%
 
-@misc{fk:Practicals,
-  author = {Florent Kirchner},
-  title = "Programmation Tacticals",
-  year  = 2003,
-  note = "{\tt http://research.nianet.org/fm-at-nia/Practicals/}"
+@book{ProofsTypes,
+  Author="Girard, J.-Y. and Y. Lafont and P. Taylor",
+  Title="Proofs and Types",
+  Publisher="Cambrige Tracts in Theoretical Computer Science, Cambridge University Press",
+  Year="1989"
 }
 
-@mastersthesis{fk:DEA,
-  author= {Florent Kirchner},
-  title= "{Towards a Common Tactical Language : The Case of Coq and PVS}",
-  school= {DEA Programmation : Sémantique, Preuves et Langages},
-  year= 2003
+@misc{Types:Dowek,
+  author = "Gilles Dowek",
+  title = "Th{\'e}orie des types",
+  year = 2002,
+  howpublished = "Lecture notes",
+  url= "http://www.lix.polytechnique.fr/~dowek/Cours/theories_des_types.ps.gz"
 }
 
-@inproceedings{fk:strata2003,
-  author= {Florent Kirchner},
-  editor= {Mila Archer et al.},
-  title= "{Coq Tacticals and PVS Strategies: A Small-Step Semantics}",
-  pages= {69-83},
-  booktitle= "{Design and Application of Strategies/Tactics in Higher Order Logics}",
-  publisher= {NASA},
-  month= "September",
-  year= 2003
+@PHDTHESIS{EGThese,
+  author = {E. Giménez},
+  title = {Un Calcul de Constructions Infinies et son application
+a la vérification de systèmes communicants},
+  type = {thèse d'Université},
+  school = {Ecole Normale Supérieure de Lyon},
+  month = {December},
+  year = {1996},
 }
 
+
 %%%%%%% Semantique %%%%%%%
 
 @misc{Sem:cours,
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 6bc5e4364..d3a408a1e 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -94,16 +94,16 @@ This is any logic which does not assume that ``A or not A''.
 
 \begin{description}
 \item[Type theory]
-Proof and Types
-Cours de Gilles
-Manuel de Coq
+Proof and Types~\cite{ProofsTypes}
+Cours de Gilles~\cite{Types:Dowek}
+Manuel de Coq~\cite{Coq:manual}
 
 \item[Inductives]
 
-Habilitation Christine
+Habilitation Christine~\cite{Pau96b}
 
 \item[Co-Inductives]
-Thèse 
+Thèse Eduardo Giménez~\cite{EGThese}
 
 \item[Extraction]
 Pierre Letouzey
@@ -212,8 +212,8 @@ Windows. The sources can be easily adapted to all platforms supporting Objective
 
 
 
-
-\section{My goal is ...,  how can I prove it ?}
+%%%%%%%
+\subsection{My goal is ...,  how can I prove it ?}
 
 
 \Question[conjonction]{My goal is a conjunction, how can I prove it ?}
@@ -297,8 +297,8 @@ You need to use the {\tt solve} tactic.
 \Question[patternmatchingsyntax]{What is the syntax for pattern matching ?}
 
 
-
-\section{\Ltac}
+%%%%%%%
+\subsection{\Ltac}
 
 \Question[ltac]{What is \Ltac ?}
 
@@ -326,8 +326,8 @@ You can use the following syntax :
 
 \Question[statdyn]{How can I define static and dynamic code ?}
 
-
-\section{Glossary}
+%%%%%%%
+\subsection{Glossary}
 
 \Question[goal]{What is a goal ?}