From 02fca80f58ddc5dda8e424702d778f07993fb4cf Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 19 Feb 2004 17:52:07 +0000 Subject: added menu entries to tactic menus --- coq/coq-abbrev.el | 66 ++++++++++++++++++++++++++++++++++++++++++++++++++----- coq/coq.el | 54 ++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 109 insertions(+), 11 deletions(-) diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index dbcaac92..9e938a2a 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -65,21 +65,30 @@ (define-abbrev-table 'coq-mode-abbrev-table '( ("a" "auto" holes-abbrev-complete 4) + ("ar" "autorewrite [ # ] using #" holes-abbrev-complete 1) ("ab" "absurd #" holes-abbrev-complete 0) ("abs" "absurd #" holes-abbrev-complete 0) ("ap" "apply #" holes-abbrev-complete 16) ("as" "assumption" holes-abbrev-complete 4) + ("ass" "assert ( # : # )" holes-abbrev-complete 4) ("au" "auto" holes-abbrev-complete 1) ("aw" "auto with #" holes-abbrev-complete 1) ("awa" "auto with arith" holes-abbrev-complete 4) ("c" "cases #" holes-abbrev-complete 1) + ("ch" "change #" holes-abbrev-complete 1) + ("chi" "change # in #" holes-abbrev-complete 1) + ("chwi" "change # with # in #" holes-abbrev-complete 1) ("con" "constructor" holes-abbrev-complete 3) + ("cong" "congruence" holes-abbrev-complete 3) ("dec" "decompose [#] #" holes-abbrev-complete 3) ("def" "Definition #:# := #." holes-abbrev-complete 5) ("def2" "Definition # (# : #) (# : #):# := #." holes-abbrev-complete 5) ("def3" "Definition # (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5) ("def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5) - ("di" "discriminate" holes-abbrev-complete 0) + ("deg" "decide equality" holes-abbrev-complete 3) + ("des" "destruct #" holes-abbrev-complete 0) + ("desu" "destruct # using #" holes-abbrev-complete 0) + ("desa" "destruct # as #" holes-abbrev-complete 0) ("dis" "discriminate" holes-abbrev-complete 0) ("e" "elim #" holes-abbrev-complete 1) ("ea" "eauto" holes-abbrev-complete 0) @@ -102,21 +111,25 @@ ("fo3" "forall (#:#) (#:#) (#:#), #" holes-abbrev-complete 0) ("fo4" "forall (#:#) (#:#) (#:#) (#:#), #" holes-abbrev-complete 0) ("fs" "Functional Scheme # := Induction for #." holes-abbrev-complete 0) + ("fsto" "firstorder" holes-abbrev-complete 0) ("fsw" "Functional Scheme # := Induction for # with #." holes-abbrev-complete 0) ("g" "generalize #" holes-abbrev-complete 0) ("ge" "generalize #" holes-abbrev-complete 0) ("gen" "generalize #" holes-abbrev-complete 0) - ("he" "Hint # : # := Extern # # #." holes-abbrev-complete 0) - ("hi" "Hint Immediate #: #." holes-abbrev-complete 0) - ("hr" "Hint Resolve #: #." holes-abbrev-complete 0) + ("hc" "Hint Constructors # : #." holes-abbrev-complete 0) + ("he" "Hint Extern # # => # : #." holes-abbrev-complete 0) + ("hi" "Hint Immediate # : #." holes-abbrev-complete 0) + ("hr" "Hint Resolve # : #." holes-abbrev-complete 0) ("hs" "Hints # : #." holes-abbrev-complete 0) - ("hu" "Hint Unfold #: #." holes-abbrev-complete 0) + ("hu" "Hint Unfold # : #." holes-abbrev-complete 0) ("i" "intro #" holes-abbrev-complete 10) ("if" "if # then # else #" holes-abbrev-complete 1) ("in" "intro" holes-abbrev-complete 1) ("ind" "induction #" holes-abbrev-complete 2) ("indv" "Inductive # : # := # : #." holes-abbrev-complete 0) + ("inj" "injection #" holes-abbrev-complete 2) ("inv" "inversion #" holes-abbrev-complete 9) + ("intu" "intuition #" holes-abbrev-complete 9) ("is" "intros #" holes-abbrev-complete 11) ("ite" "if # then # else #" holes-abbrev-complete 1) ("l" "Lemma # : #." holes-abbrev-complete 4) @@ -124,21 +137,62 @@ ("o" "omega" holes-abbrev-complete 0) ("om" "Omega" holes-abbrev-complete 0) ("p" "Print #" holes-abbrev-complete 3) + ("po" "pose ( # := # )" nil 0) ("pr" "print #" holes-abbrev-complete 2) + ("rep" "replace # with #" holes-abbrev-complete 19) ("r" "rewrite #" holes-abbrev-complete 19) ("r<" "rewrite <- #" holes-abbrev-complete 0) + ("rl" "rewrite <- #" holes-abbrev-complete 0) + ("refl" "reflexivity #" holes-abbrev-complete 0) + ("ri" "rewrite # in #" holes-abbrev-complete 19) + ("ril" "rewrite <- # in #" holes-abbrev-complete 0) ("re" "rewrite #" holes-abbrev-complete 0) ("re<" "rewrite <- #" holes-abbrev-complete 0) + ("ring" "ring #" holes-abbrev-complete 19) ("s" "simpl" holes-abbrev-complete 23) + ("set" "set ( # := #)" holes-abbrev-complete 23) + ("seth" "set ( # := #) in * |-" holes-abbrev-complete 23) + ("setg" "set ( # := #) in |-*" holes-abbrev-complete 23) + ("seti" "set ( # := #) in #" holes-abbrev-complete 23) + ("su" "subst #" holes-abbrev-complete 23) ("sc" "Scheme # := Induction for # Sort #." nil 0) ("si" "simpl" holes-abbrev-complete 0) ("sp" "Split" holes-abbrev-complete 1) ("sy" "symmetry" holes-abbrev-complete 0) ("sym" "symmetry" holes-abbrev-complete 0) ("t" "trivial" holes-abbrev-complete 1) - ("tr" "trivial" holes-abbrev-complete 7) + ("tr" "trivial" holes-abbrev-complete 1) + ("trans" "transitivity #" holes-abbrev-complete 1) + ("ta" "tauto" holes-abbrev-complete 1) ("u" "unfold #" holes-abbrev-complete 1) ("un" "unfold #" holes-abbrev-complete 7) + + ("mt" "Module Type # := #." holes-abbrev-complete 0) + ("mti" "Module Type #. +# +End #." holes-abbrev-complete 0) + ("mo" "Module # : # := #." holes-abbrev-complete 0) + ("mo2" "Module # <: # := #." holes-abbrev-complete 0) + ("moi" "Module # : #. +# +End #." holes-abbrev-complete 0) + ("moi2" "Module # <: #. +# +End #." holes-abbrev-complete 0) + + + ("dm" "Declare Module # : # := #." holes-abbrev-complete 0) + ("dm2" "Declare Module # <: # := #." holes-abbrev-complete 0) + ("dmi" "Declare Module # : #. +# +End #." holes-abbrev-complete 0) + ("dmi2" "Declare Module # <: #. +# +End #." holes-abbrev-complete 0) + + + + ("m" "match # with # => #" holes-abbrev-complete 1) ("m2" "match # with diff --git a/coq/coq.el b/coq/coq.el index b36f1dc0..d9691d7e 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -85,6 +85,7 @@ ;; ----- coq specific menu +;TODO: build the command submenu automatically from abbrev table (defpgdefault menu-entries '( ("Insert Command" @@ -92,14 +93,26 @@ ["Definition def" (insert-and-expand "def") t] ["Fixpoint fix" (insert-and-expand "fix") t] ["Functional Scheme fs" (insert-and-expand "fs") t] - ["Functional Scheme w fs" (insert-and-expand "fs") t] + ["Functional Scheme w fsw" (insert-and-expand "fsw") 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] ["Lemma l" (insert-and-expand "l") 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] + ["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] @@ -124,39 +137,70 @@ ["match2 m2" (insert-and-expand "m2") t] ["match3 m3" (insert-and-expand "m3") t] ["match4 m4" (insert-and-expand "m4") t] - ["match5 m5" (insert-and-expand "m5") t] ) - ("Insert tactic" + ("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] - ["discriminate di" (insert-and-expand "di") 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] - ["trivial tr" (insert-and-expand "tr") t] + ["tauto ta" (insert-and-expand "ta") t] ["unfold u" (insert-and-expand "u") t] ) -- cgit v1.2.3