diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-20 17:18:18 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-20 17:18:18 +0000 |
| commit | 0f4f723a5608075ff4aa48290314df30843efbcb (patch) | |
| tree | 09316ca71749b9218972ca801356388c04d29b4c /ide/coq.mli | |
| parent | c6b9d70f9292fc9f4b5f272b5b955af0e8fe0bea (diff) | |
Declarative Proof Language: main commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 3 |
1 files changed, 3 insertions, 0 deletions
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 |