From d5442f9a05c87295a3bb46409a228ba73c11da8f Mon Sep 17 00:00:00 2001
From: narboux
Date: Thu, 1 Apr 2004 15:43:41 +0000
Subject: *** empty log message ***

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

(limited to 'doc')

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 3141888f0e..c1476d40cf 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -515,12 +515,38 @@ Qed.
 
 \end{coq_example}
 
+\Question[autowith]{My goal is solvable by  some lemma within a set of lemmas and I don't want to remember which one, how can I prove it ?}
 
+You can use a what is called a ``base of Hints''.
+
+\begin{coq_example}
+Require Import ZArith.
+Require Ring.
+Open Local Scope Z_scope.
+
+Lemma toto1 : 1+1 = 2.
+ring.
+Qed.
+
+Lemma toto2 : 2+2 = 4.
+ring.
+Qed.
+
+Lemma toto3 : 2+1 = 3.
+ring.
+Qed.
+
+Hint Resolve toto1 toto2 toto3 : mybase.
+
+Goal 2+(1+1)=4. 
+auto with mybase.
+Qed.
+\end{coq_example}
 
-\Question[autowith]{My goal is solvable by  some lemma within a set of lemmas and I don't want to remember which one, how can I prove it ?}
 
-Use a base of Hints.
+\Question[savedqed]{What is the difference between saved qed and defined ?}
 
+\Question[opaquetrans]{What is the difference between opaque and transparent ?}
 
 
 \Question[assumption]{My goal is one of the hypothesis, how can I prove it ?}
-- 
cgit v1.2.3