Add transparent_abstract tactic

1 files changed, 9 insertions, 5 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 9378529cb..46274e12f 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,17 @@ 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.
+\item \texttt{transparent\_abstract {\tacexpr}}.\\
+  Save the subproof in a transparent lemma rather than an opaque one.
+\item \texttt{transparent\_abstract {\tacexpr} using {\ident}}.\\
+  Give explicitly the name of the auxiliary transparent lemma.
 \end{Variants}
 
 \ErrMsg \errindex{Proof is not complete}