From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001 From: Jason Gross 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 From 84845f766d9b9d532f615352fbc8a0e78e1727e9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 27 Mar 2017 13:28:17 -0400 Subject: Mark transparent_abstract as risky in docs As per Enrico's request. --- doc/refman/RefMan-ltac.tex | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 46274e12f..c2f52e23b 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1121,10 +1121,17 @@ 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} -- cgit v1.2.3