From 8d337f3c87976b2254531186cda2cbe0844bd727 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 10 Mar 2004 00:37:33 +0000 Subject: added a menu for hole operations --- coq/coq.el | 207 ++++++++++++++++++++++++++++++++----------------------------- 1 file changed, 109 insertions(+), 98 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 4bc20706..ce233856 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -91,126 +91,137 @@ '( ("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] + ["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] + ["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] "" - ["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] + ["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] "" - ["Scheme sc" (insert-and-expand "sc") t] - ["Functional Scheme fs" (insert-and-expand "fs") t] - ["Functional Scheme with fsw" (insert-and-expand "fsw") t] + ["Scheme sc" (insert-and-expand "sc") t] + ["Functional Scheme fs" (insert-and-expand "fs") t] + ["Functional Scheme with fsw" (insert-and-expand "fsw") t] "" - ["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 extern he" (insert-and-expand "he") t] - ["hints hs" (insert-and-expand "hs") t] + ["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 extern he" (insert-and-expand "he") t] + ["hints hs" (insert-and-expand "hs") t] "" - ["infix inf" (insert-and-expand "inf") t] + ["infix inf" (insert-and-expand "inf") 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] + ["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] + ["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 ab" (insert-and-expand "ab") t] - ["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] + ["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 "r") t] - ["rewrite <- rl" (insert-and-expand "r") t] - ["rewrite <- in ril" (insert-and-expand "r") 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] + ["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 "r") t] + ["rewrite <- rl" (insert-and-expand "r") t] + ["rewrite <- in ril" (insert-and-expand "r") 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 #??" (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] + ["What are those holes?" (holes-short-doc) t] + ) ["expand abbrev at point" expand-abbrev t] ["list abbrevs" list-abbrevs t] ["Insert Section..." coq-insert-section t] -- cgit v1.2.3