diff options
| -rw-r--r-- | doc/newfaq/main.tex | 19 |
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. %%%%%%% |