Reset a dangling proof in the FAQ.

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 8495156ca1..b03aa64090 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -755,19 +755,19 @@ the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}).
  E.g. in this case (this occurs only in the {\tt Set}-impredicative
  variant of \Coq):
 
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
 \begin{coq_example*}
 Inductive I : Type :=
   intro : forall k:Set, k -> I.
-Lemma eq_jdef : 
+Lemma eq_jdef :
    forall x y:nat, intro _ x = intro _ y -> x = y.
 Proof.
    intros x y H; injection H.
 \end{coq_example*}
 
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
  Injectivity of constructors is restricted to predicative types. If
 injectivity on large inductive types were not restricted, we would be
 allowed to derive an inconsistency (e.g. following the lines of