added menu entries to tactic menus

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<ctrl-backspace>" (insert-and-expand "def") t]
      ["Fixpoint              fix<ctrl-backspace>" (insert-and-expand "fix") t]
      ["Functional Scheme     fs<ctrl-backspace>" (insert-and-expand "fs") t]
-     ["Functional Scheme w   fs<ctrl-backspace>" (insert-and-expand "fs") t]
+     ["Functional Scheme w   fsw<ctrl-backspace>" (insert-and-expand "fsw") t]
      ["Inductive             indv<ctrl-backspace>" (insert-and-expand "indv") t]
      ["Inductive1            indv1<ctrl-backspace>" (insert-and-expand "indv1") t]
      ["Inductive2             indv2<ctrl-backspace>" (insert-and-expand "indv2") t]
      ["Inductive3            indv3<ctrl-backspace>" (insert-and-expand "indv3") t]
      ["Inductive4            indv4<ctrl-backspace>" (insert-and-expand "indv4") t]
      ["Lemma                 l<ctrl-backspace>" (insert-and-expand "l") t]
+     ["Module                mo<ctrl-backspace>" (insert-and-expand "mo") t]
+     ["Module (<:)           mo2<ctrl-backspace>" (insert-and-expand "mo") t]
+     ["Module (interactive)  moi<ctrl-backspace>" (insert-and-expand "moi") t]
+     ["Module (interactive <:) moi2<ctrl-backspace>" (insert-and-expand "moi2") t]
+     ["Module Type           mt<ctrl-backspace>" (insert-and-expand "mt") t]
+     ["Module Type (interactive) mti<ctrl-backspace>" (insert-and-expand "mti") t]
+     ["Declare Module        dm<ctrl-backspace>" (insert-and-expand "dm") t]
+     ["Declare Module (<:)   dm2<ctrl-backspace>" (insert-and-expand "dm") t]
+     ["Declare Module (inter.) dmi<ctrl-backspace>" (insert-and-expand "dmi") t]
+     ["Declare Module (inter. <:) dmi2<ctrl-backspace>" (insert-and-expand "dmi2") t]
+
      ["Scheme                sc<ctrl-backspace>" (insert-and-expand "sc") t]
+     ["hint Constructors     hc<ctrl-backspace>" (insert-and-expand "hc") t]
      ["hint Immediate        hi<ctrl-backspace>" (insert-and-expand "hi") t]
      ["hint Resolve          hr<ctrl-backspace>" (insert-and-expand "hr") t]
      ["hint extern           he<ctrl-backspace>" (insert-and-expand "he") t]
@@ -124,39 +137,70 @@
      ["match2        m2<ctrl-backspace>"  (insert-and-expand "m2") t]
      ["match3        m3<ctrl-backspace>"  (insert-and-expand "m3") t]
      ["match4        m4<ctrl-backspace>"  (insert-and-expand "m4") t]
-     ["match5        m5<ctrl-backspace>"  (insert-and-expand "m5") t]
      )
 
-    ("Insert tactic" 
+    ("Insert tactic (a-f)" 
      "TACTIC           ABBREVIATION"
      ["absurd                 ab<ctrl-bacspace>"  (insert-and-expand "ab") t]
      ["absurd                 abs<ctrl-bacspace>"  (insert-and-expand "abs") t]
      ["assumption             as<ctrl-bacspace>"  (insert-and-expand "as") t]
+     ["assert                 ass<ctrl-bacspace>"  (insert-and-expand "ass") t]
      ["auto                   a<ctrl-bacspace>"  (insert-and-expand "a") t]
      ["auto with              aw<ctrl-bacspace>"  (insert-and-expand "aw") t]
      ["auto with arith        awa<ctrl-bacspace>"  (insert-and-expand "awa") t]
+     ["autorewrite            ar<ctrl-bacspace>"  (insert-and-expand "ar") t]
      ["cases                  c<ctrl-bacspace>"  (insert-and-expand "c") t]
+     ["change                 ch<ctrl-bacspace>"  (insert-and-expand "ch") t]
+     ["change in              chi<ctrl-bacspace>"  (insert-and-expand "chi") t]
+     ["change with in         chwi<ctrl-bacspace>"  (insert-and-expand "chwi") t]
+     ["constructor            con<ctrl-bacspace>"  (insert-and-expand "con") t]
+     ["congruence             cong<ctrl-bacspace>"  (insert-and-expand "cong") t]
      ["decompose              dec<ctrl-bacspace>"  (insert-and-expand "dec") t]
-     ["discriminate           di<ctrl-bacspace>"  (insert-and-expand "di") t]
+     ["decide equality        deg<ctrl-bacspace>"  (insert-and-expand "deg") t]
+     ["destruct               des<ctrl-bacspace>"  (insert-and-expand "des") t]
+     ["destruct using         desu<ctrl-bacspace>"  (insert-and-expand "desu") t]
+     ["destruct as            desa<ctrl-bacspace>"  (insert-and-expand "desa") t]
+     ["discriminate           dis<ctrl-bacspace>"  (insert-and-expand "dis") t]
      ["eauto                  ea<ctrl-bacspace>"  (insert-and-expand "ea") t]
      ["eauto with             eaw<ctrl-bacspace>"  (insert-and-expand "dec") t]
      ["elim                   e<ctrl-bacspace>"  (insert-and-expand "e") t]
      ["elim using             elu<ctrl-bacspace>"  (insert-and-expand "elu") t]
      ["exists                 ex<ctrl-bacspace>"  (insert-and-expand "ex") t]
+     ["field                  fld<ctrl-bacspace>"  (insert-and-expand "fld") t]
+     ["firstorder             fsto<ctrl-bacspace>"  (insert-and-expand "fsto") t]
+     ["fourier                fou<ctrl-bacspace>"  (insert-and-expand "fou") t]
      ["functional induction   fi<ctrl-bacspace>"  (insert-and-expand "fi") t]
+     )
+
+    ("Insert tactic (g-z)" 
+     "TACTIC           ABBREVIATION"
      ["generalize             g<ctrl-bacspace>"  (insert-and-expand "g") t]
      ["induction              ind<ctrl-bacspace>"  (insert-and-expand "ind") t]
+     ["injection              inj<ctrl-bacspace>"  (insert-and-expand "inj") t]
      ["intro                  i<ctrl-bacspace>"  (insert-and-expand "i") t]
      ["intros                 is<ctrl-bacspace>"  (insert-and-expand "is") t]
+     ["intuition              intu<ctrl-bacspace>"  (insert-and-expand "intu") t]
      ["inversion              inv<ctrl-bacspace>"  (insert-and-expand "inv") t]
      ["omega                  om<ctrl-bacspace>"  (insert-and-expand "om") t]
+     ["pose                   po<ctrl-bacspace>"  (insert-and-expand "om") t]
+     ["reflexivity            refl<ctrl-bacspace>"  (insert-and-expand "refl") t]
+     ["replace                rep<ctrl-bacspace>"  (insert-and-expand "rep") t]
      ["rewrite                r<ctrl-bacspace>"  (insert-and-expand "r") t]
+     ["rewrite in             ri<ctrl-bacspace>"  (insert-and-expand "r") t]
+     ["rewrite <-             rl<ctrl-bacspace>"  (insert-and-expand "r") t]
+     ["rewrite <- in          ril<ctrl-bacspace>"  (insert-and-expand "r") t]
+     ["set                    set<ctrl-bacspace>"  (insert-and-expand "set") t]
+     ["set in hyp             seth<ctrl-bacspace>"  (insert-and-expand "seth") t]
+     ["set in goal            setg<ctrl-bacspace>"  (insert-and-expand "setg") t]
+     ["set in                 seti<ctrl-bacspace>"  (insert-and-expand "seti") t]
      ["simpl                  s<ctrl-bacspace>"  (insert-and-expand "s") t]
      ["simpl                  si<ctrl-bacspace>"  (insert-and-expand "si") t]
      ["split                  sp<ctrl-bacspace>"  (insert-and-expand "sp") t]
+     ["subst                  su<ctrl-bacspace>"  (insert-and-expand "su") t]
      ["symmetry               sym<ctrl-bacspace>"  (insert-and-expand "sym") t]
+     ["transitivity           trans<ctrl-bacspace>"  (insert-and-expand "trans") t]
      ["trivial                t<ctrl-bacspace>"  (insert-and-expand "t") t]
-     ["trivial                tr<ctrl-bacspace>"  (insert-and-expand "tr") t]
+     ["tauto                  ta<ctrl-bacspace>"  (insert-and-expand "ta") t]
      ["unfold                 u<ctrl-bacspace>"  (insert-and-expand "u") t]
      )