*** empty log message ***

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

1 files changed, 19 insertions, 0 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 5e89785db3..089f9ae862 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -61,6 +61,10 @@
 \def\symmetry{{\tt symmetry }}
 \def\Focus{{\tt Focus }}
 \def\discriminate{{\tt discriminate }}
+\def\contradiction{{\tt contradiction }}
+\def\intuition{{\tt intuition }}
+
+
 
 \begin{document}
 \bibliographystyle{plain}
@@ -432,6 +436,11 @@ apply mylemma.
 Qed.
 \end{coq_example}
 
+\Question[falseimpliesall]{My goal contains False as an hypotheses, how can I prove it ?}
+
+You can use the \contradiction or \intuition tactics.
+
+
 \Question[reflexivity]{My goal is an equality of two convertible terms, how can I prove it ?}
 
 Just use the \reflexivity tactic.
@@ -851,6 +860,16 @@ while Assert is.
 
 \Question[vector]{How can I define vectors of size n ?}
 
+\Question[autospeed]{How can I speed up \auto ?}
+
+You can use info \auto to replace \auto by the tactics it generates.
+You can split your hint bases into smaller ones.
+
+\Question[evaluable]{Can you explain me what an evaluable constant is ?}
+
+\Question[Tauto]{What is the equivalent of Tauto for classical logic ?}
+
+Currently there are no equivalent tactic for classical logic.
 
 
 %%%%%%%