Proof using cleanup, small doc addition and fix using Type in collections

Fix #12930

3 files changed, 25 insertions, 12 deletions

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`.
diff --git a/test-suite/bugs/closed/bug_12930.v b/test-suite/bugs/closed/bug_12930.v
new file mode 100644
index 0000000000..e2a524301a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12930.v
@@ -0,0 +1,10 @@
+Section S.
+  Variable v : Prop.
+  Variable vv : v.
+  Collection easy := Type*.
+
+  Lemma ybar : v.
+  Proof using easy.
+    exact vv.
+  Qed.
+End S.
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 2130a398e9..95680c2a4e 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -41,28 +41,27 @@ let set_of_type env ty =
 let full_set env =
   List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
 
-let rec process_expr env e ty =
+let process_expr env e v_ty =
   let rec aux = function
     | SsEmpty -> Id.Set.empty
-    | SsType -> set_of_type env ty
-    | SsSingl { CAst.v = id } -> set_of_id env id
+    | SsType -> v_ty
+    | SsSingl { CAst.v = id } -> set_of_id id
     | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
     | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
     | SsCompl e -> Id.Set.diff (full_set env) (aux e)
     | SsFwdClose e -> close_fwd env (aux e)
+  and set_of_id id =
+    if Id.to_string id = "All" then
+      full_set env
+    else if CList.mem_assoc_f Id.equal id !known_names then
+      aux (CList.assoc_f Id.equal id !known_names)
+    else Id.Set.singleton id
   in
-    aux e
-
-and set_of_id env id =
-  if Id.to_string id = "All" then
-    List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
-  else if CList.mem_assoc_f Id.equal id !known_names then
-    process_expr env (CList.assoc_f Id.equal id !known_names) []
-  else Id.Set.singleton id
+  aux e
 
 let process_expr env e ty =
   let v_ty = set_of_type env ty in
-  let s = Id.Set.union v_ty (process_expr env e ty) in
+  let s = Id.Set.union v_ty (process_expr env e v_ty) in
   Id.Set.elements s
 
 let name_set id expr = known_names := (id,expr) :: !known_names