From f6cea698f19766087fa56b16ed8dc8cedf079643 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 23 May 2016 11:12:28 +0200
Subject: STM: proof block detection for bullets and { block }

---
 engine/proofview.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine')

diff --git a/engine/proofview.mli b/engine/proofview.mli
index 7996b7969..93ba55c61 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -303,6 +303,9 @@ val guard_no_unifiable : Names.Name.t list option tactic
     goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
 
+(** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
+val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool
+
 (** [with_shelf tac] executes [tac] and returns its result together with the set
     of goals shelved by [tac]. The current shelf is unchanged. *)
 val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
-- 
cgit v1.2.3