From 91dfe5163fd4405977ad8fc8fe178ba5bcd73c88 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 15 Mar 2019 19:16:30 +0100
Subject: [doc] [abstract] Document a bit some problems with abstract.

---
 doc/sphinx/proof-engine/ltac.rst | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 52e3029b8f..0322b43694 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1071,6 +1071,16 @@ Proving a subgoal as a separate lemma
    It may be useful to generate lemmas minimal w.r.t. the assumptions they
    depend on. This can be obtained thanks to the option below.
 
+   .. warning::
+
+      The abstract tactic, while very useful, still has some known
+      limitations, see https://github.com/coq/coq/issues/9146 for more
+      details. Thus we recommend using it caution in some
+      "non-standard" contexts. In particular, ``abstract`` won't
+      properly work when used inside quotations ``ltac:(...)``, or
+      if used as part of typeclass resolution, it may produce wrong
+      terms when in universe polymorphic mode.
+
    .. tacv:: abstract @expr using @ident
 
       Give explicitly the name of the auxiliary lemma.
-- 
cgit v1.2.3