aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide_ui.ml
diff options
context:
space:
mode:
authorGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2015-06-19 12:53:51 +0200
committerGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2016-06-02 09:17:38 +0200
commit6cc27d2ca57a5d2fedfa52d8b44c37c60ccb6988 (patch)
tree4d30728dd551ccede5284e301feea86bf78d32d7 /ide/coqide_ui.ml
parentcf5baeccf3cf7c24ccc69aa728bfe836fba5230a (diff)
Add a [Show Proof.] query to CoqIDE.
Diffstat (limited to 'ide/coqide_ui.ml')
-rw-r--r--ide/coqide_ui.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index edfe28b26..65735240a 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -119,6 +119,7 @@ let init () =
<menuitem action='About' />
<menuitem action='Locate' />
<menuitem action='Print Assumptions' />
+ <menuitem action='Show Proof' />
</menu>
<menu name='Tools' action='Tools'>
<menuitem action='Comment' />