From 62bbd0d2bc33d53ec4c46b424de0587eaca7c1d6 Mon Sep 17 00:00:00 2001
From: narboux
Date: Fri, 2 Apr 2004 16:30:28 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8528 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/newfaq/main.tex | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'doc')

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.
 
 
 %%%%%%%
-- 
cgit v1.2.3