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

---
 vernac/declare.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'vernac')

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