From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 10 Jun 2016 19:12:49 -0400
Subject: Add transparent_abstract tactic

---
 doc/refman/RefMan-ltac.tex | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'doc/refman')

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