diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-26 08:54:28 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-26 08:54:28 +0000 |
| commit | ea1eaa9b152b73652f417e02bd469e5b289cec47 (patch) | |
| tree | 4d654ad1434bac0781eb4f3e6f1505c3895df4ba /ide/coq.mli | |
| parent | 40425048feff138e6c67555c7ee94142452d1cae (diff) | |
fin des conclusions multiples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 7b43a0c95..991f104db 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -33,7 +33,7 @@ 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_pm_goal : unit -> goal val get_current_goals_nb : unit -> int |