aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-05-23 11:12:28 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-06 05:48:44 -0400
commitf6cea698f19766087fa56b16ed8dc8cedf079643 (patch)
tree1880e497e1f4228cabf4e712c80fd9ff5b2ad3d0 /engine
parent5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 (diff)
STM: proof block detection for bullets and { block }
Diffstat (limited to 'engine')
-rw-r--r--engine/proofview.mli3
1 files changed, 3 insertions, 0 deletions
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