From 0f4f723a5608075ff4aa48290314df30843efbcb Mon Sep 17 00:00:00 2001
From: corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 20 Sep 2006 17:18:18 +0000
Subject: Declarative Proof Language: main commit

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

(limited to 'ide/coq.mli')

diff --git a/ide/coq.mli b/ide/coq.mli
index b6c0ed89c..7b43a0c95 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -27,11 +27,14 @@ val is_state_preserving : Vernacexpr.vernac_expr -> bool
 
 type hyp = env * evar_map * 
            ((identifier*string) * constr option * constr) * (string * string)
+type meta = env * evar_map * string
 type concl = env * evar_map * constr * string
 type goal = hyp list * concl
 
 val get_current_goals : unit -> goal list
 
+val get_current_pm_goal : unit -> hyp list * meta list
+
 val get_current_goals_nb : unit -> int
 
 val print_no_goal : unit -> string
-- 
cgit v1.2.3