aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2004-02-19 09:24:26 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2004-02-19 09:24:26 +0000
commitc02a7c93c801487a3f283ee1bbaf0e85b6f6006b (patch)
tree374c4b97e3e0fcd0fe245d0f5d84ad0979c5e9ae /coq
parent3ec47057dda331a80be71310c5d335b84f697796 (diff)
added some menu entries for coq.
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el4
1 files changed, 3 insertions, 1 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 117debb5..804db615 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -95,7 +95,9 @@
["Search isos/pattern..." coq-SearchIsos t]
["expand abbrev at point" expand-abbrev t]
["list abbrevs" list-abbrevs t]
- ["What are those #??" (holes-short-doc)]
+ ["What are those #??" (holes-short-doc) t]
+ ["insert Fixpoint" (insert-and-expand "fix") t]
+ ["insert Definition" (insert-and-expand "def") t]
["3 buffers view" coq-three-b t]
["Begin Section..." coq-begin-Section t]
["End Section" coq-end-Section t]