From fd9d10f2c7eff9ff72f42e9ecd3ffd5179de4da0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 12 Oct 2020 16:52:47 +0200
Subject: [stm] support #[using] attribute

---
 stm/stm.ml                            |  5 +++--
 test-suite/success/definition_using.v | 22 ++++++++++++++++++++++
 vernac/declare.mli                    |  4 ++++
 3 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 85f889c879..df7e35beb5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2275,8 +2275,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
               ), true, true
           | `MaybeASync (start, nodes, name, delegate) -> (fun () ->
                 reach ~cache:true start;
-                (* no sections *)
-                if CList.is_empty (Environ.named_context (Global.env ()))
+                if CList.is_empty (Environ.named_context (Global.env ())) (* no sections *)
+                   || PG_compat.get_pstate () |> (* #[using] attribute *)
+                        Option.cata (fun x -> Option.has_some (Declare.Proof.get_used_variables x)) false
                 then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) ()
                 else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) ()
               ), not redefine_qed, true
diff --git a/test-suite/success/definition_using.v b/test-suite/success/definition_using.v
index a8eab93404..120e62b145 100644
--- a/test-suite/success/definition_using.v
+++ b/test-suite/success/definition_using.v
@@ -44,3 +44,25 @@ Check c4 : bogus -> bool.
 Check c5 : bogus -> nat -> bool.
 Check c6 : bogus -> bool.
 Check c7 : bogus -> nat -> bool.
+
+Section B.
+
+Variable a : bogus.
+Variable h : c1 a = true.
+
+#[using="a*"]
+Definition c8 : bogus := a.
+
+Collection ccc := a h.
+
+#[using="ccc"]
+Definition c9 : bogus := a.
+
+#[using="ccc - h"]
+Definition c10 : bogus := a.
+
+End B.
+
+Check c8 : forall a, c1 a = true -> bogus.
+Check c9 : forall a, c1 a = true -> bogus.
+Check c10: bogus -> bogus.
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 8e6456d834..0520bf8717 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -245,6 +245,10 @@ module Proof : sig
    * (w.r.t. type dependencies and let-ins covered by it) *)
   val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t
 
+  (** Gets the set of variables declared to be used by the proof. None means
+      no "Proof using" or #[using] was given *)
+  val get_used_variables : t -> Id.Set.t option
+
   (** Compacts the representation of the proof by pruning all intermediate
       terms *)
   val compact : t -> t
-- 
cgit v1.2.3