From 4791a7e43e5bb3dba154265abf3caa684663db83 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 19 Mar 2004 12:58:29 +0000 Subject: coq < 8.0 menu and abbrevs. --- coq/coq.el | 174 +++---------------------------------------------------------- 1 file changed, 6 insertions(+), 168 deletions(-) (limited to 'coq/coq.el') diff --git a/coq/coq.el b/coq/coq.el index d4c779f2..f8f3beff 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -84,174 +84,12 @@ :group 'coq) -;; ----- coq specific menu - -;TODO: build the command submenu automatically from abbrev table -(defpgdefault menu-entries - '( - ("Insert Command" - "COMMAND ABBREVIATION" - ["Definition def" (insert-and-expand "def") t] - ["Fixpoint fix" (insert-and-expand "fix") t] - ["Lemma l" (insert-and-expand "l") t] - "" - ["Inductive indv" (insert-and-expand "indv") t] - ["Inductive1 indv1" (insert-and-expand "indv1") t] - ["Inductive2 indv2" (insert-and-expand "indv2") t] - ["Inductive3 indv3" (insert-and-expand "indv3") t] - ["Inductive4 indv4" (insert-and-expand "indv4") t] - "" - ["Section..." coq-insert-section t] - "" - ("Modules" - "COMMAND ABBREVIATION" - ["Module (interactive)... " coq-insert-module t] - ["Module mo" (insert-and-expand "mo") t] - ["Module (<:) mo2" (insert-and-expand "mo") t] -; ["Module (interactive) moi" (insert-and-expand "moi") t] -; ["Module (interactive <:) moi2" (insert-and-expand "moi2") t] - ["Module Type mt" (insert-and-expand "mt") t] -; ["Module Type (interactive) mti" (insert-and-expand "mti") t] -; "" - ["Declare Module dm" (insert-and-expand "dm") t] - ["Declare Module (<:) dm2" (insert-and-expand "dm") t] -; ["Declare Module (inter.) dmi" (insert-and-expand "dmi") t] -; ["Declare Module (inter. <:) dmi2" (insert-and-expand "dmi2") t] - ) - ("Hints" - "COMMAND ABBREVIATION" - ["Hint Constructors hc" (insert-and-expand "hc") t] - ["Hint Immediate hi" (insert-and-expand "hi") t] - ["Hint Resolve hr" (insert-and-expand "hr") t] - ["Hint Rewrite hrw" (insert-and-expand "hrw") t] - ["Hint Extern he" (insert-and-expand "he") t] - ) - ("Schemes" - "COMMAND ABBREVIATION" - ["Scheme sc" (insert-and-expand "sc") t] - ["Functional Scheme fs" (insert-and-expand "fs") t] - ["Functional Scheme with fsw" (insert-and-expand "fsw") t] - ) - ("Notations" - "COMMAND ABBREVIATION" - ["infix inf" (insert-and-expand "inf") t] - ["Notation (no assoc) nota" (insert-and-expand "nota") t] - ["Notation (assoc) notas" (insert-and-expand "notas") t] - ["Notation (no assoc, scope) notasc" (insert-and-expand "notasc") t] - ["Notation (assoc, scope) notassc" (insert-and-expand "notassc") t] - ) - ) - - ("Insert term" - "FORM ABBREVIATION" - ["forall fo" (insert-and-expand "fo") t] - ["forall1 fo1" (insert-and-expand "fo1") t] - ["forall2 fo2" (insert-and-expand "fo2") t] - ["forall3 fo3" (insert-and-expand "fo3") t] - ["forall4 fo4" (insert-and-expand "fo4") t] - "" - ["fun f" (insert-and-expand "f") t] - ["fun1 f1" (insert-and-expand "f1") t] - ["fun2 f2" (insert-and-expand "f2") t] - ["fun3 f3" (insert-and-expand "f3") t] - ["fun4 f4" (insert-and-expand "f4") t] - "" - ["if then else if" (insert-and-expand "li") t] - ["let in li" (insert-and-expand "li") t] - "" - ["match m" (insert-and-expand "m") t] - ["match2 m2" (insert-and-expand "m2") t] - ["match3 m3" (insert-and-expand "m3") t] - ["match4 m4" (insert-and-expand "m4") t] - ) - - ("Insert tactic (a-f)" - "TACTIC ABBREVIATION" - ["absurd abs" (insert-and-expand "abs") t] - ["assumption as" (insert-and-expand "as") t] - ["assert ass" (insert-and-expand "ass") t] - ["auto a" (insert-and-expand "a") t] - ["auto with aw" (insert-and-expand "aw") t] - ["auto with arith awa" (insert-and-expand "awa") t] - ["autorewrite ar" (insert-and-expand "ar") t] - ["cases c" (insert-and-expand "c") t] - ["change ch" (insert-and-expand "ch") t] - ["change in chi" (insert-and-expand "chi") t] - ["change with in chwi" (insert-and-expand "chwi") t] - ["constructor con" (insert-and-expand "con") t] - ["congruence cong" (insert-and-expand "cong") t] - ["decompose dec" (insert-and-expand "dec") t] - ["decide equality deg" (insert-and-expand "deg") t] - ["destruct des" (insert-and-expand "des") t] - ["destruct using desu" (insert-and-expand "desu") t] - ["destruct as desa" (insert-and-expand "desa") t] - ["discriminate dis" (insert-and-expand "dis") t] - ["eauto ea" (insert-and-expand "ea") t] - ["eauto with eaw" (insert-and-expand "dec") t] - ["elim e" (insert-and-expand "e") t] - ["elim using elu" (insert-and-expand "elu") t] - ["exists ex" (insert-and-expand "ex") t] - ["field fld" (insert-and-expand "fld") t] - ["firstorder fsto" (insert-and-expand "fsto") t] - ["fourier fou" (insert-and-expand "fou") t] - ["functional induction fi" (insert-and-expand "fi") t] - ) - - ("Insert tactic (g-z)" - "TACTIC ABBREVIATION" - ["generalize g" (insert-and-expand "g") t] - ["induction ind" (insert-and-expand "ind") t] - ["injection inj" (insert-and-expand "inj") t] - ["intro i" (insert-and-expand "i") t] - ["intros is" (insert-and-expand "is") t] - ["intuition intu" (insert-and-expand "intu") t] - ["inversion inv" (insert-and-expand "inv") t] - ["omega om" (insert-and-expand "om") t] - ["pose po" (insert-and-expand "om") t] - ["reflexivity refl" (insert-and-expand "refl") t] - ["replace rep" (insert-and-expand "rep") t] - ["rewrite r" (insert-and-expand "r") t] - ["rewrite in ri" (insert-and-expand "ri") t] - ["rewrite <- r<" (insert-and-expand "rl") t] - ["rewrite <- in ri<" (insert-and-expand "ril") t] - ["set set" (insert-and-expand "set") t] - ["set in hyp seth" (insert-and-expand "seth") t] - ["set in goal setg" (insert-and-expand "setg") t] - ["set in seti" (insert-and-expand "seti") t] - ["simpl s" (insert-and-expand "s") t] - ["simpl si" (insert-and-expand "si") t] - ["split sp" (insert-and-expand "sp") t] - ["subst su" (insert-and-expand "su") t] - ["symmetry sym" (insert-and-expand "sym") t] - ["transitivity trans" (insert-and-expand "trans") t] - ["trivial t" (insert-and-expand "t") t] - ["tauto ta" (insert-and-expand "ta") t] - ["unfold u" (insert-and-expand "u") t] - ) - - ["What are those highlighted chars??" (holes-short-doc) t] - ("holes" - "make a hole active click on it" - "disable a hole click on it (button 2)" - "destroy a hole click on it (button 3)" - "make a hole with mouse C-M-select" - ["make a hole at point C-M-h" (set-make-active-hole) t] - ["make selection a hole C-M-h" (set-make-active-hole) t] - ["replace active hole by selection C-M-y" (replace-update-active-hole) t] - "replace active hole with mouse C-M-Shift select" - ["jump to active hole M-return" (set-point-next-hole-destroy) t] - ["forget all holes in this buffer" (clear-all-buffer-holes) t] - ["What are those holes?" (holes-short-doc) t] - ) - ["expand abbrev at point" expand-abbrev t] - ["list abbrevs" list-abbrevs t] - ["Print..." coq-Print t] - ["Check..." coq-Check t] - ["Hints" coq-PrintHint t] - ["Show ith goal..." coq-Show t] - ["Search isos/pattern..." coq-SearchIsos t] - ["3 buffers view" coq-three-b t] - ["Compile" coq-Compile t] )) +;; ----- coq specific menu is defined in coq-abbrev.el + +(cond + (coq-version-is-V8 (require 'coq-abbrev)) + (t (require 'coq-abbrev-V7)) + ) -- cgit v1.2.3