From df6d411a7f9aecdd3794fa837d425ff280a153a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 28 Aug 2020 14:31:34 +0200
Subject: Proof using cleanup, small doc addition and fix using Type in
 collections

Fix #12930
---
 doc/sphinx/proof-engine/proof-handling.rst | 4 ++++
 1 file changed, 4 insertions(+)

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

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 4480b10319..55e4f26fe8 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -156,6 +156,10 @@ list of assertion commands is given in :ref:`Assertions`. The command
    ``T``, then the commands ``Proof using a`` and ``Proof using T a``
    are equivalent.
 
+   The set of declared variables always includes the variables used by
+   the statement. In other words ``Proof using e`` is equivalent to
+   ``Proof using Type + e`` for any declaration expression ``e``.
+
    .. cmdv:: Proof using {+ @ident } with @tactic
 
       Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`.
-- 
cgit v1.2.3