*** empty log message ***

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

1 files changed, 29 insertions, 15 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 56a8078663..3bb6ecf061 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -530,6 +530,9 @@ scripts won't be modular. If you add some hyphothesis to your theorem
 (or change their order), you will have to change your proof to adapt
 to the new names.
 
+\Question[namedintrosbis]{How can I automatize that ?}
+
+You can use the {\tt Show Intro.} command to generate the names and use your editor to generate a fully named \intro tactic. 
 
 \Question[assert]{I want to state a fact that I will use later as an hypothesis, how can I do it ?}
 
@@ -574,7 +577,6 @@ Qed.
 \Question[subgoalsorder]{How can I change the order of the subgoals ?}
 
 
-
 \Question[hyphotesisorder]{How can I change the order of the hypothesis ?}
 
 You can use the {\tt move ... after} command.
@@ -605,6 +607,9 @@ You should use the \eapply tactic.
 Sometime you can use the \abstractt tactic, which makes as if you had
 stated one intermediated lemmas, this speeds up the typing process.
 
+\Question[admitted]{How can use a proof which is not finished ?}
+
+You can use the {\tt Admitted} command to state your current proof as an axiom.
 
 %%%%%%%
 \subsection{\Ltac}
@@ -695,6 +700,25 @@ that is still unknown.
 
 \Question[dependanttype]{What is a dependent type ?}
 
+
+\Question[reflection]{What is a proof by reflection ?}
+
+This is a proof generated by some computation which is done using the
+internal reduction of Coq (not using the tactic language of \Coq
+(\Ltac) nor the implementation language for \Coq).  An example of
+tactic using the reflection mechanism is the \ring tactic. The
+reflection method consist in reflecting a subset of Coq language (for
+example the arithmetical expressions) into an object of the Coq
+language itself (in this case an inductive type denoting arithmetical
+expressions).  For more information see~\cite{howe,harrison,boutin}
+and the last chapter of the Coq'Art.
+
+
+\Question[irrelevance]{What is proof-irrelevance ?}
+
+
+\section{Publishing tools}
+
 \Question[coqlatex]{How can I generate some latex from my development ?}
 
 \Question[coqhtml]{How can I generate some HTML from my development ?}
@@ -703,12 +727,14 @@ that is still unknown.
 
 \Question[coqtex]{How can I cite some \Coq in my latex document ?}
 
-\Question[coqidedescr]{What is \CoqIde ?}
 
-\Question[irrelevance]{What is proof-irrelevance ?}
+\section{CoqIde}
 
+\Question[coqidedescr]{What is \CoqIde ?}
 
 
+\section{Extraction}
+
 \Question[extraction]{What is program extraction ?}
 
 Program extraction consist in generating a prgram from a constructive proof.
@@ -721,18 +747,6 @@ You can extract your programs to Objective Caml and Haskell.
 
 You can provide programs for your axioms.
 
-\Question[reflection]{What is a proof by reflection ?}
-
-This is a proof generated by some computation which is done using the
-internal reduction of Coq (not using the tactic language of \Coq
-(\Ltac) nor the implementation language for \Coq).  An example of
-tactic using the reflection mechanism is the \ring tactic. The
-reflection method consist in reflecting a subset of Coq language (for
-example the arithmetical expressions) into an object of the Coq
-language itself (in this case an inductive type denoting arithmetical
-expressions).  For more information see~\cite{howe,harrison,boutin}
-and the last chapter of the Coq'Art.
-
 
 \section{Conclusion and Farewell.}
 \label{ccl}