diff options
| author | narboux | 2004-03-26 14:51:27 +0000 |
|---|---|---|
| committer | narboux | 2004-03-26 14:51:27 +0000 |
| commit | 8e0436ac1c37f0fbd00c19b4754bf571929029d0 (patch) | |
| tree | 79d4502fd0811f3fa9da78049d8b9ab1df242836 | |
| parent | e785cbde0da95bb85d2ee5dcd6ae8d7893649acd (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8509 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/newfaq/main.tex | 14 | ||||
| -rwxr-xr-x | doc/newfaq/run.sh | 2 |
2 files changed, 16 insertions, 0 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index c71a3b12c6..726f3e6be9 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -6,6 +6,9 @@ \usepackage{stmaryrd} \usepackage{amssymb} \usepackage{url} +\usepackage{fullpage} +%\usepackage{hevea} +\input{../macros.tex} % version et date \def\faqversion{0.1} @@ -274,6 +277,13 @@ Use a base of Hints. Use the {\tt assumption} tactic. +\begin{coq_example} +Goal 1=1 -> 1=1. +intro. +assumption. +Qed. +\end{coq_example} + \Question[trivial]{My goal is ???, how can I prove it ?} \Question[proofwith]{I want to automatize the use of some tactic how can I do it ?} @@ -296,6 +306,10 @@ You need to use the {\tt solve} tactic. \Question[patternmatchingsyntax]{What is the syntax for pattern matching ?} +\Question[abstract]{What can I do when {\tt Qed.} is slow ?} + +Sometime you can use the {\tt abstract} tactic, which makes as if you had stated intermediated lemmas, this speeds up the typing process. + %%%%%%% \subsection{\Ltac} diff --git a/doc/newfaq/run.sh b/doc/newfaq/run.sh new file mode 100755 index 0000000000..1ceecf77fb --- /dev/null +++ b/doc/newfaq/run.sh @@ -0,0 +1,2 @@ +#/bin/sh +coq-tex main.tex & latex main.v.tex
\ No newline at end of file |