From d0ec5640994fefe6674c5abb6f7c7001305073cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 28 Jul 2015 15:32:59 +0200
Subject: Reset a dangling proof in the FAQ.

---
 doc/faq/FAQ.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc')

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