From bc77234dc5d40d4540793ceead1595b15ab18bb8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 14 Feb 2015 15:11:29 +0100
Subject: dependent destruction: Fix (part of) bug #3961, by fixing dependent *
 generalizing * which was broken since 8.4.

---
 doc/refman/RefMan-tacex.tex | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 668a68c9c7..9f4ddc8044 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -247,7 +247,7 @@ to simplify equalities appearing at the beginning of induction
 hypotheses, generally using trivial applications of
 reflexivity. In cases where the equality is not between constructor
 forms though, one must help the automation by giving
-some arguments, using the {\tt specialize} tactic.
+some arguments, using the {\tt specialize} tactic for example.
 
 \begin{coq_example*}
 destruct D... apply weak ; apply ax. apply ax.
@@ -257,16 +257,24 @@ destruct D...
 Show.
 \end{coq_example}
 \begin{coq_example}
-  specialize (IHterm G empty).
+  specialize (IHterm G0 empty eq_refl).
 \end{coq_example}
 
-Then the automation can find the needed equality {\tt G = G} to narrow
-the induction hypothesis further. This concludes our example.
+Once the induction hypothesis has been narrowed to the right equality,
+it can be used directly. 
 
 \begin{coq_example}
-  simpl_depind.
+  apply weak, IHterm.
 \end{coq_example}
 
+If there is an easy first-order solution to these equations as in this subgoal, the
+{\tt specialize\_eqs} tactic can be used instead of giving explicit proof
+terms:
+
+\begin{coq_example}
+  specialize_eqs IHterm.
+\end{coq_example}
+This concludes our example.
 \SeeAlso The induction \ref{elim}, case \ref{case} and inversion \ref{inversion} tactics.
 
 \section[\tt autorewrite]{\tt autorewrite\label{autorewrite-example}}
-- 
cgit v1.2.3


From 4a53151f846476f2fbe038a4ecb8e84256a26ba9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 14 Feb 2015 18:35:04 +0100
Subject: Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior

Of course such proofs cannot be processed asynchronously
---
 doc/refman/RefMan-ltac.tex | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 689ac14254..1704b4d60b 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1010,13 +1010,19 @@ Fail all:let n:= numgoals in guard n=2.
 Reset Initial.
 \end{coq_eval}
 
-\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed export}
 \index{Tacticals!abstract@{\tt abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
 current goal and \textit{n} is chosen so that this is a fresh name.
+Such auxiliary lemma is inlined in the final proof term
+unless the proof is ended with ``\texttt{Qed export}''.  In such
+case the lemma is preserved.  The syntax
+``\texttt{Qed export }\ident$_1$\texttt{, ..., }\ident$_n$''
+is also supported.  In such case the system checks that the names given by the
+user actually exist when the proof is ended.
 
 This tactical is useful with tactics such as \texttt{omega} or
 \texttt{discriminate} that generate huge proof terms. With that tool
-- 
cgit v1.2.3