*** empty log message ***

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

1 files changed, 16 insertions, 0 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 9b679c828..56a807866 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -699,11 +699,27 @@ that is still unknown.
 
 \Question[coqhtml]{How can I generate some HTML from my development ?}
 
+\Question[depgraph]{How can I generate some dependancy graph from my development ?}
+
 \Question[coqtex]{How can I cite some \Coq in my latex document ?}
 
 \Question[coqidedescr]{What is \CoqIde ?}
 
+\Question[irrelevance]{What is proof-irrelevance ?}
+
+
+
+\Question[extraction]{What is program extraction ?}
+
+Program extraction consist in generating a prgram from a constructive proof.
+
+\Question[extraclang]{Which language can I extract to ?}
+
+You can extract your programs to Objective Caml and Haskell.
+
+\Question[extraaxiom]{How can I change extract an incomplete proof ?}
 
+You can provide programs for your axioms.
 
 \Question[reflection]{What is a proof by reflection ?}