diff options
| -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 |