From 267d7a63e9c24573226d0890bedb783f10dcb235 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 12 Oct 2014 15:32:38 +0200
Subject: Adding a tactic which fails if one of the goals under focus is
 dependent in another one.

---
 proofs/goal.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'proofs/goal.ml')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 631c2428e..4a1b6bfc0 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -35,6 +35,8 @@ let pr_goal {content = e} = str "GOAL:" ++ Pp.int (Evar.repr e)
 
 let goal_ident sigma {content = e} = Evd.evar_ident e sigma
 
+let dependent_goal_ident sigma {content = e} = Evd.dependent_evar_ident e sigma
+
 (* access primitive *)
 (* invariant : [e] must exist in [em] *)
 let content evars { content = e } = Evd.find evars e
-- 
cgit v1.2.3