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 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'stm')

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
-- 
cgit v1.2.3