Merge PR#201: Transparent abstract

1 files changed, 16 insertions, 5 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 9378529cb..c2f52e23b 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1087,8 +1087,8 @@ 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}\comindex{Qed exporting}
-\index{Tacticals!abstract@{\tt abstract}}}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract}\comindex{Qed exporting}
+\index{Tacticals!abstract@{\tt abstract}}\index{Tacticals!transparent\_abstract@{\tt transparent\_abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
@@ -1114,13 +1114,24 @@ on. This can be obtained thanks to the option below.
 {\tt Set Shrink Abstract}
 \end{quote}
 
-When set, all lemmas generated through \texttt{abstract {\tacexpr}} are
-quantified only over the variables that appear in the term constructed by
-\texttt{\tacexpr}.
+When set, all lemmas generated through \texttt{abstract {\tacexpr}}
+and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the
+variables that appear in the term constructed by \texttt{\tacexpr}.
 
 \begin{Variants}
 \item \texttt{abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary lemma.
+  Use this feature at your own risk; explicitly named and reused subterms
+  don't play well with asynchronous proofs.
+\item \texttt{transparent\_abstract {\tacexpr}}.\\
+  Save the subproof in a transparent lemma rather than an opaque one.
+  Use this feature at your own risk; building computationally relevant terms
+  with tactics is fragile.
+\item \texttt{transparent\_abstract {\tacexpr} using {\ident}}.\\
+  Give explicitly the name of the auxiliary transparent lemma.
+  Use this feature at your own risk; building computationally relevant terms
+  with tactics is fragile, and explicitly named and reused subterms
+  don't play well with asynchronous proofs.
 \end{Variants}
 
 \ErrMsg \errindex{Proof is not complete}