From 7b2bf4785916803c24629239aa746706fe3f6ef6 Mon Sep 17 00:00:00 2001
From: aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 23 Nov 2011 17:09:11 +0000
Subject: In emacs mode, prints a list of the dependent existential variables
 introduced during the proof together with information whether they were
 (partially) instantiated and if it's the case the list of existential
 variables that were used to that effect.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14721 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'proofs/proof.mli')

diff --git a/proofs/proof.mli b/proofs/proof.mli
index b4c84cbf6..d80ac79af 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -171,6 +171,9 @@ module V82 : sig
   val depth : proof -> int 
 
   val top_goal : proof -> Goal.goal Evd.sigma
+  
+  (* returns the existential variable used to start the proof *)
+  val top_evars : proof -> Evd.evar list
 
   (* Implements the Existential command *)
   val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit
-- 
cgit v1.2.3