From 8e0436ac1c37f0fbd00c19b4754bf571929029d0 Mon Sep 17 00:00:00 2001
From: narboux
Date: Fri, 26 Mar 2004 14:51:27 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8509 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/newfaq/main.tex | 14 ++++++++++++++
 doc/newfaq/run.sh   |  2 ++
 2 files changed, 16 insertions(+)
 create mode 100755 doc/newfaq/run.sh

(limited to 'doc')

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