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(+)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 46274e12f3..c2f52e23bc 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