*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8524 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 39 insertions, 0 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 3aabb98416..3141888f0e 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -479,6 +479,44 @@ Qed.
 \end{coq_example}
 
 
+\Question[eapplyeauto]{My goal would be solvable using {\tt apply;assumption} if It would not create meta-variables, how can I prove it ?}
+
+You can use {\tt eapply yourtheorem;eauto} but it won't work in all cases ! (for example if more than one hypotheses match one of the sub goals generated by \eapply) so you should rather use  {\tt try solve [eapply yourtheorem;eauto]}, otherwise some metavariables may be incorrectly instanciated.
+
+\begin{coq_example}
+Lemma trans : forall x y z : nat, x=y -> y=z -> x=z.
+intros.
+transitivity y;assumption.
+Qed.
+
+Goal forall x y z : nat, x=y -> y=z -> x=z.
+intros.
+eapply trans;eauto.
+Qed.
+
+Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z.
+intros.
+eapply trans;eauto.
+Undo.
+eapply trans.
+apply H.
+auto.
+Qed.
+
+Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z.
+intros.
+eapply trans;eauto.
+Undo.
+try solve [eapply trans;eauto].
+eapply trans.
+apply H.
+auto.
+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.
@@ -725,6 +763,7 @@ that is still unknown.
 
 \Question[lemmasvstheorem]{What is difference between a lemma, a fact  and a theorem ?}
 
+
 \Question[organize]{How can I organize my proofs ?}
 
 \Question[dependanttype]{What is a dependent type ?}