coq < 8.0 menu and abbrevs.

4 files changed, 448 insertions, 175 deletions

diff --git a/coq/coq-abbrev-V7.el b/coq/coq-abbrev-V7.el
new file mode 100644
index 00000000..f9f37651
--- /dev/null
+++ b/coq/coq-abbrev-V7.el
@@ -0,0 +1,262 @@
+;; default abbrev table
+; This is for coq V7, you should test coq version before loading
+
+;#s are replaced by holes by holes-abbrev-complete
+(if (boundp 'holes-abbrev-complete)
+	 ()
+  (define-abbrev-table 'coq-mode-abbrev-table
+	 '(
+		("a" "Auto" holes-abbrev-complete 4)
+		("ar" "Autorewrite [@{db,db...}] using @{tac}" 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)
+		("au" "Auto" holes-abbrev-complete 1)
+		("aw" "Auto with " holes-abbrev-complete 1)
+		("awa" "Auto with arith" holes-abbrev-complete 4)
+		("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)
+		("dec" "Decompose [#] @{hyp}" holes-abbrev-complete 3)
+		("def" "Definition #:# := #." holes-abbrev-complete 5)
+		("def1" "Definition # [# : #] :# := #." holes-abbrev-complete 5)
+		("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)
+		("dm" "Declare Module # : # := #." holes-abbrev-complete 0)
+		("dm2" "Declare Module # <: # := #." holes-abbrev-complete 0)
+		("dmi" "Declare Module # : #.\n#\nEnd #." holes-abbrev-complete 0)
+		("dmi2" "Declare Module # <: #.\n#\nEnd #." holes-abbrev-complete 0)
+		("e" "Elim #" holes-abbrev-complete 1)
+		("ea" "Eauto" holes-abbrev-complete 0)
+		("eap" "Eapply #" holes-abbrev-complete 0)
+		("eaw" "Eauto with @{db}" holes-abbrev-complete 0)
+		("eawa" "Eauto with arith" holes-abbrev-complete 0)
+		("el" "Elim #" holes-abbrev-complete 0)
+		("elu" "Elim # using #" holes-abbrev-complete 0)
+		("ex" "Exists #" holes-abbrev-complete 0)
+		("f" "[#:#]#" holes-abbrev-complete 0)
+		("fix" "Fixpoint # [#:#] : # :=\n#." holes-abbrev-complete 3)
+		("fo" "(#:#)#" holes-abbrev-complete 0)
+		("fsto" "Firstorder" holes-abbrev-complete 0)
+		("g" "Generalize #" holes-abbrev-complete 0)
+		("ge" "Generalize #" holes-abbrev-complete 0)
+		("gen" "Generalize #" holes-abbrev-complete 0)
+		("hc" "Hints Constructors # : #." holes-abbrev-complete 0)
+		("he" "Hint # : @{db} := Extern @{cost} (@{pat}) (@{tac})." holes-abbrev-complete 0)
+		("hi" "Hints Immediate # : @{db}." holes-abbrev-complete 0)
+		("hr" "Hints Resolve # : @{db}." holes-abbrev-complete 0)
+		("hrw" "Hint Rewrite -> [@{t1 t2...}] in @{db} using @{tac}." holes-abbrev-complete 0)
+		("hs" "Hints # : #." holes-abbrev-complete 0)
+		("hu" "Hints 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)
+		("indv2" "Inductive # : # :=\n| # : #\n| # : #." holes-abbrev-complete 0)
+		("indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
+		("indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0)
+		("indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." 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)
+		("li" "Let # := # in #" holes-abbrev-complete 1)
+		("c" "Cases # of\n| # => #\nend" holes-abbrev-complete 1)
+		("c2" "Cases # of\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
+		("c3" "Cases # of\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
+		("c4" "Cases # of\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
+		("c5" "Cases # of\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1)
+		("mt" "Module Type # := #." holes-abbrev-complete 0)
+		("mti" "Module Type #.\n#\nEnd #." holes-abbrev-complete 0)
+		("mo" "Module # : # := #." holes-abbrev-complete 0)
+		("mo2" "Module # <: # := #." holes-abbrev-complete 0)
+		("moi" "Module # : #.\n#\nEnd #." holes-abbrev-complete 0)
+		("moi2" "Module # <: #.\n#\nEnd #." holes-abbrev-complete 0)
+		("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)
+		("ri<" "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)
+		("su" "Subst #" holes-abbrev-complete 23)
+		("sc" "Scheme @{name} := 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 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)
+		("v" "Variable # : #." holes-abbrev-complete 7)
+		("vs" "Variables # : #." holes-abbrev-complete 7)
+		)
+	 )
+  )
+
+
+(defpgdefault menu-entries
+  '(
+    ("Insert Command" 
+      "COMMAND               ABBREVIATION"
+     ["Definition            def<C-BS>" (insert-and-expand "def") t]
+     ["Fixpoint              fix<C-BS>" (insert-and-expand "fix") t]
+     ["Lemma                 l<C-BS>" (insert-and-expand "l") t]
+     ""
+     ["Inductive             indv<C-BS>" (insert-and-expand "indv") t]
+     ["Inductive1            indv1<C-BS>" (insert-and-expand "indv1") t]
+     ["Inductive2             indv2<C-BS>" (insert-and-expand "indv2") t]
+     ["Inductive3            indv3<C-BS>" (insert-and-expand "indv3") t]
+     ["Inductive4            indv4<C-BS>" (insert-and-expand "indv4") t]
+     ""
+     ["Section..." coq-insert-section t]
+     ""
+     ("Modules"
+      "COMMAND               ABBREVIATION"
+      ["Module (interactive)... " coq-insert-module t]
+      ["Module                mo<C-BS>" (insert-and-expand "mo") t]
+      ["Module (<:)           mo2<C-BS>" (insert-and-expand "mo") t]
+;      ["Module (interactive)  moi<C-BS>" (insert-and-expand "moi") t]
+;      ["Module (interactive <:) moi2<C-BS>" (insert-and-expand "moi2") t]
+      ["Module Type           mt<C-BS>" (insert-and-expand "mt") t]
+;      ["Module Type (interactive) mti<C-BS>" (insert-and-expand "mti") t]
+;      ""
+      ["Declare Module        dm<C-BS>" (insert-and-expand "dm") t]
+      ["Declare Module (<:)   dm2<C-BS>" (insert-and-expand "dm") t]
+;      ["Declare Module (inter.) dmi<C-BS>" (insert-and-expand "dmi") t]
+;      ["Declare Module (inter. <:) dmi2<C-BS>" (insert-and-expand "dmi2") t]
+      )
+     ("Hints"
+      "COMMAND               ABBREVIATION"
+      ["Hint Constructors     hc<C-BS>" (insert-and-expand "hc") t]
+      ["Hint Immediate        hi<C-BS>" (insert-and-expand "hi") t]
+      ["Hint Resolve          hr<C-BS>" (insert-and-expand "hr") t]
+      ["Hint Rewrite          hrw<C-BS>" (insert-and-expand "hrw") t]
+      ["Hint Extern           he<C-BS>" (insert-and-expand "he") t]
+     )
+     ("Schemes"
+      "COMMAND               ABBREVIATION"
+      ["Scheme                sc<C-BS>" (insert-and-expand "sc") t]
+      )
+     )
+
+    ("Insert term" 
+     "FORM           ABBREVIATION"
+     ["forall        fo<C-BS>"  (insert-and-expand "fo") t]
+     ""
+     ["fun           f<ctrl-bacspace>"  (insert-and-expand "f") t]
+     ""
+     ["let in        li<C-BS>"  (insert-and-expand "li") t]
+     ""
+     ["Cases         c<C-BS>"  (insert-and-expand "c") t]
+     ["Cases2        c2<C-BS>"  (insert-and-expand "c2") t]
+     ["Cases3        c3<C-BS>"  (insert-and-expand "c3") t]
+     ["Cases4        c4<C-BS>"  (insert-and-expand "c4") t]
+     )
+
+    ("Insert tactic (a-f)" 
+     "TACTIC           ABBREVIATION"
+     ["Absurd                 abs<C-BS>"  (insert-and-expand "abs") t]
+     ["Assumption              as<C-BS>"  (insert-and-expand "as") t]
+     ["Assert                 ass<C-BS>"  (insert-and-expand "ass") t]
+     ["Auto                     a<C-BS>"  (insert-and-expand "a") t]
+     ["Auto with               aw<C-BS>"  (insert-and-expand "aw") t]
+     ["Auto with arith        awa<C-BS>"  (insert-and-expand "awa") t]
+     ["Autorewrite             ar<C-BS>"  (insert-and-expand "ar") t]
+     ["Cases                    c<C-BS>"  (insert-and-expand "c") t]
+     ["Change                  ch<C-BS>"  (insert-and-expand "ch") t]
+     ["Change in              chi<C-BS>"  (insert-and-expand "chi") t]
+     ["Change with in        chwi<C-BS>"  (insert-and-expand "chwi") t]
+     ["Constructor            con<C-BS>"  (insert-and-expand "con") t]
+     ["Congruence            cong<C-BS>"  (insert-and-expand "cong") t]
+     ["Decompose              dec<C-BS>"  (insert-and-expand "dec") t]
+     ["Decide Equality        deg<C-BS>"  (insert-and-expand "deg") t]
+     ["Destruct               des<C-BS>"  (insert-and-expand "des") t]
+     ["Destruct using        desu<C-BS>"  (insert-and-expand "desu") t]
+     ["Destruct as           desa<C-BS>"  (insert-and-expand "desa") t]
+     ["Discriminate           dis<C-BS>"  (insert-and-expand "dis") t]
+     ["Eauto                   ea<C-BS>"  (insert-and-expand "ea") t]
+     ["Eauto with             eaw<C-BS>"  (insert-and-expand "dec") t]
+     ["Elim                     e<C-BS>"  (insert-and-expand "e") t]
+     ["Elim using             elu<C-BS>"  (insert-and-expand "elu") t]
+     ["Exists                  ex<C-BS>"  (insert-and-expand "ex") t]
+     ["Field                  fld<C-BS>"  (insert-and-expand "fld") t]
+     ["Firstorder            fsto<C-BS>"  (insert-and-expand "fsto") t]
+     ["Fourier                fou<C-BS>"  (insert-and-expand "fou") t]
+     )
+
+    ("Insert tactic (g-z)" 
+     "TACTIC           ABBREVIATION"
+     ["Generalize             g<C-BS>"  (insert-and-expand "g") t]
+     ["Induction              ind<C-BS>"  (insert-and-expand "ind") t]
+     ["Injection              inj<C-BS>"  (insert-and-expand "inj") t]
+     ["Intro                  i<C-BS>"  (insert-and-expand "i") t]
+     ["Intros                 is<C-BS>"  (insert-and-expand "is") t]
+     ["Intuition              intu<C-BS>"  (insert-and-expand "intu") t]
+     ["Inversion              inv<C-BS>"  (insert-and-expand "inv") t]
+     ["Omega                  om<C-BS>"  (insert-and-expand "om") t]
+     ["Pose                   po<C-BS>"  (insert-and-expand "om") t]
+     ["Reflexivity            refl<C-BS>"  (insert-and-expand "refl") t]
+     ["Replace                rep<C-BS>"  (insert-and-expand "rep") t]
+     ["Rewrite                r<C-BS>"  (insert-and-expand "r") t]
+     ["Rewrite in             ri<C-BS>"  (insert-and-expand "ri") t]
+     ["Rewrite <-             r<<C-BS>"  (insert-and-expand "rl") t]
+     ["Rewrite <- in          ri<<C-BS>"  (insert-and-expand "ril") t]
+     ["Simpl                  s<C-BS>"  (insert-and-expand "s") t]
+     ["Simpl                  si<C-BS>"  (insert-and-expand "si") t]
+     ["Split                  sp<C-BS>"  (insert-and-expand "sp") t]
+     ["Subst                  su<C-BS>"  (insert-and-expand "su") t]
+     ["Symmetry               sym<C-BS>"  (insert-and-expand "sym") t]
+     ["Transitivity           trans<C-BS>"  (insert-and-expand "trans") t]
+     ["Trivial                t<C-BS>"  (insert-and-expand "t") t]
+     ["Tauto                  ta<C-BS>"  (insert-and-expand "ta") t]
+     ["Unfold                 u<C-BS>"  (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] ))
+
+(provide 'coq-abbrev-V7)
+
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 3a088c95..58e1d216 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -1,8 +1,5 @@
 ;; default abbrev table
-; This is for coq V8, Should test coq version
-;(defvar coq-version-is-V74 nil)
-;(defvar coq-version-is-V7 nil)
-;(defvar coq-version-is-V6 nil)
+; This is for coq V8, you should test coq version before loading
 
 ;#s are replaced by holes by holes-abbrev-complete
 (if (boundp 'holes-abbrev-complete)
@@ -105,7 +102,7 @@
 		("notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." holes-abbrev-complete 0)
 		("notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." holes-abbrev-complete 0)
 		("o" "omega" holes-abbrev-complete 0)
-		("om" "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)
@@ -143,4 +140,172 @@
 	 )
   )
 
+;TODO: build the command submenu automatically from abbrev table
+(defpgdefault menu-entries
+  '(
+    ("Insert Command" 
+      "COMMAND               ABBREVIATION"
+     ["Definition            def<C-BS>" (insert-and-expand "def") t]
+     ["Fixpoint              fix<C-BS>" (insert-and-expand "fix") t]
+     ["Lemma                 l<C-BS>" (insert-and-expand "l") t]
+     ""
+     ["Inductive             indv<C-BS>" (insert-and-expand "indv") t]
+     ["Inductive1            indv1<C-BS>" (insert-and-expand "indv1") t]
+     ["Inductive2             indv2<C-BS>" (insert-and-expand "indv2") t]
+     ["Inductive3            indv3<C-BS>" (insert-and-expand "indv3") t]
+     ["Inductive4            indv4<C-BS>" (insert-and-expand "indv4") t]
+     ""
+     ["Section..." coq-insert-section t]
+     ""
+     ("Modules"
+      "COMMAND               ABBREVIATION"
+      ["Module (interactive)... " coq-insert-module t]
+      ["Module                mo<C-BS>" (insert-and-expand "mo") t]
+      ["Module (<:)           mo2<C-BS>" (insert-and-expand "mo") t]
+;      ["Module (interactive)  moi<C-BS>" (insert-and-expand "moi") t]
+;      ["Module (interactive <:) moi2<C-BS>" (insert-and-expand "moi2") t]
+      ["Module Type           mt<C-BS>" (insert-and-expand "mt") t]
+;      ["Module Type (interactive) mti<C-BS>" (insert-and-expand "mti") t]
+;      ""
+      ["Declare Module        dm<C-BS>" (insert-and-expand "dm") t]
+      ["Declare Module (<:)   dm2<C-BS>" (insert-and-expand "dm") t]
+;      ["Declare Module (inter.) dmi<C-BS>" (insert-and-expand "dmi") t]
+;      ["Declare Module (inter. <:) dmi2<C-BS>" (insert-and-expand "dmi2") t]
+      )
+     ("Hints"
+      "COMMAND               ABBREVIATION"
+      ["Hint Constructors     hc<C-BS>" (insert-and-expand "hc") t]
+      ["Hint Immediate        hi<C-BS>" (insert-and-expand "hi") t]
+      ["Hint Resolve          hr<C-BS>" (insert-and-expand "hr") t]
+      ["Hint Rewrite          hrw<C-BS>" (insert-and-expand "hrw") t]
+      ["Hint Extern           he<C-BS>" (insert-and-expand "he") t]
+     )
+     ("Schemes"
+      "COMMAND               ABBREVIATION"
+      ["Scheme                sc<C-BS>" (insert-and-expand "sc") t]
+      ["Functional Scheme     fs<C-BS>" (insert-and-expand "fs") t]
+      ["Functional Scheme with    fsw<C-BS>" (insert-and-expand "fsw") t]
+      )
+     ("Notations"
+      "COMMAND               ABBREVIATION"
+      ["infix                           inf<C-BS>" (insert-and-expand "inf") t]     
+      ["Notation (no assoc)             nota<C-BS>" (insert-and-expand "nota") t]     
+      ["Notation (assoc)                notas<C-BS>" (insert-and-expand "notas") t]     
+      ["Notation (no assoc, scope)      notasc<C-BS>" (insert-and-expand "notasc") t]     
+      ["Notation (assoc, scope)         notassc<C-BS>" (insert-and-expand "notassc") t]
+      )
+     )
+
+    ("Insert term" 
+     "FORM           ABBREVIATION"
+     ["forall        fo<C-BS>"  (insert-and-expand "fo") t]
+     ["forall1       fo1<C-BS>"  (insert-and-expand "fo1") t]
+     ["forall2       fo2<C-BS>" (insert-and-expand "fo2") t]
+     ["forall3       fo3<C-BS>" (insert-and-expand "fo3") t]
+     ["forall4       fo4<C-BS>" (insert-and-expand "fo4") t]
+     ""
+     ["fun           f<ctrl-bacspace>"  (insert-and-expand "f") t]
+     ["fun1          f1<ctrl-bacspace>"  (insert-and-expand "f1") t]
+     ["fun2          f2<C-BS>" (insert-and-expand "f2") t]
+     ["fun3          f3<C-BS>" (insert-and-expand "f3") t]
+     ["fun4          f4<C-BS>" (insert-and-expand "f4") t]
+     ""
+     ["if then else  if<C-BS>"  (insert-and-expand "li") t]
+     ["let in        li<C-BS>"  (insert-and-expand "li") t]
+     ""
+     ["match         m<C-BS>"  (insert-and-expand "m") t]
+     ["match2        m2<C-BS>"  (insert-and-expand "m2") t]
+     ["match3        m3<C-BS>"  (insert-and-expand "m3") t]
+     ["match4        m4<C-BS>"  (insert-and-expand "m4") t]
+     )
+
+    ("Insert tactic (a-f)" 
+     "TACTIC           ABBREVIATION"
+     ["absurd                 abs<C-BS>"  (insert-and-expand "abs") t]
+     ["assumption              as<C-BS>"  (insert-and-expand "as") t]
+     ["assert                 ass<C-BS>"  (insert-and-expand "ass") t]
+     ["auto                     a<C-BS>"  (insert-and-expand "a") t]
+     ["auto with               aw<C-BS>"  (insert-and-expand "aw") t]
+     ["auto with arith        awa<C-BS>"  (insert-and-expand "awa") t]
+     ["autorewrite             ar<C-BS>"  (insert-and-expand "ar") t]
+     ["cases                    c<C-BS>"  (insert-and-expand "c") t]
+     ["change                  ch<C-BS>"  (insert-and-expand "ch") t]
+     ["change in              chi<C-BS>"  (insert-and-expand "chi") t]
+     ["change with in        chwi<C-BS>"  (insert-and-expand "chwi") t]
+     ["constructor            con<C-BS>"  (insert-and-expand "con") t]
+     ["congruence            cong<C-BS>"  (insert-and-expand "cong") t]
+     ["decompose              dec<C-BS>"  (insert-and-expand "dec") t]
+     ["decide equality        deg<C-BS>"  (insert-and-expand "deg") t]
+     ["destruct               des<C-BS>"  (insert-and-expand "des") t]
+     ["destruct using        desu<C-BS>"  (insert-and-expand "desu") t]
+     ["destruct as           desa<C-BS>"  (insert-and-expand "desa") t]
+     ["discriminate           dis<C-BS>"  (insert-and-expand "dis") t]
+     ["eauto                   ea<C-BS>"  (insert-and-expand "ea") t]
+     ["eauto with             eaw<C-BS>"  (insert-and-expand "dec") t]
+     ["elim                     e<C-BS>"  (insert-and-expand "e") t]
+     ["elim using             elu<C-BS>"  (insert-and-expand "elu") t]
+     ["exists                  ex<C-BS>"  (insert-and-expand "ex") t]
+     ["field                  fld<C-BS>"  (insert-and-expand "fld") t]
+     ["firstorder            fsto<C-BS>"  (insert-and-expand "fsto") t]
+     ["fourier                fou<C-BS>"  (insert-and-expand "fou") t]
+     ["functional induction    fi<C-BS>"  (insert-and-expand "fi") t]
+     )
+
+    ("Insert tactic (g-z)" 
+     "TACTIC           ABBREVIATION"
+     ["generalize             g<C-BS>"  (insert-and-expand "g") t]
+     ["induction              ind<C-BS>"  (insert-and-expand "ind") t]
+     ["injection              inj<C-BS>"  (insert-and-expand "inj") t]
+     ["intro                  i<C-BS>"  (insert-and-expand "i") t]
+     ["intros                 is<C-BS>"  (insert-and-expand "is") t]
+     ["intuition              intu<C-BS>"  (insert-and-expand "intu") t]
+     ["inversion              inv<C-BS>"  (insert-and-expand "inv") t]
+     ["omega                  om<C-BS>"  (insert-and-expand "om") t]
+     ["pose                   po<C-BS>"  (insert-and-expand "om") t]
+     ["reflexivity            refl<C-BS>"  (insert-and-expand "refl") t]
+     ["replace                rep<C-BS>"  (insert-and-expand "rep") t]
+     ["rewrite                r<C-BS>"  (insert-and-expand "r") t]
+     ["rewrite in             ri<C-BS>"  (insert-and-expand "ri") t]
+     ["rewrite <-             r<<C-BS>"  (insert-and-expand "rl") t]
+     ["rewrite <- in          ri<<C-BS>"  (insert-and-expand "ril") t]
+     ["set                    set<C-BS>"  (insert-and-expand "set") t]
+     ["set in hyp             seth<C-BS>"  (insert-and-expand "seth") t]
+     ["set in goal            setg<C-BS>"  (insert-and-expand "setg") t]
+     ["set in                 seti<C-BS>"  (insert-and-expand "seti") t]
+     ["simpl                  s<C-BS>"  (insert-and-expand "s") t]
+     ["simpl                  si<C-BS>"  (insert-and-expand "si") t]
+     ["split                  sp<C-BS>"  (insert-and-expand "sp") t]
+     ["subst                  su<C-BS>"  (insert-and-expand "su") t]
+     ["symmetry               sym<C-BS>"  (insert-and-expand "sym") t]
+     ["transitivity           trans<C-BS>"  (insert-and-expand "trans") t]
+     ["trivial                t<C-BS>"  (insert-and-expand "t") t]
+     ["tauto                  ta<C-BS>"  (insert-and-expand "ta") t]
+     ["unfold                 u<C-BS>"  (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] ))
+
+(provide 'coq-abbrev)
 
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 82d13924..80e0cdb1 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -101,9 +101,17 @@ version of coq by doing 'coqtop -v'."  )
 			 (message v7) 
 			 (setq coq-version-is-V7 t)
 			 (setq coq-version-is-V74 nil))
-			((string-match num "\\<8"))
+			((string-match num "\\<7.4") 
+			 (message v74)
+			 (setq coq-version-is-V74 t)
+			 (setq coq-version-is-V7 t) )
+			((string-match num "\\<8") 
+			 (message (concat "falling back to default: " v8))
+			 (setq coq-version-is-V8 t)
+			 (setq coq-version-is-V7 t) 
+			 (setq coq-version-is-V74 t))			
 			(t 
-			 (message v8) 
+			 (message (concat "falling back to default: " v8))
 			 (setq coq-version-is-V8 t)
 			 (setq coq-version-is-V7 t) 
 			 (setq coq-version-is-V74 t)))))))))
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<C-BS>" (insert-and-expand "def") t]
-     ["Fixpoint              fix<C-BS>" (insert-and-expand "fix") t]
-     ["Lemma                 l<C-BS>" (insert-and-expand "l") t]
-     ""
-     ["Inductive             indv<C-BS>" (insert-and-expand "indv") t]
-     ["Inductive1            indv1<C-BS>" (insert-and-expand "indv1") t]
-     ["Inductive2             indv2<C-BS>" (insert-and-expand "indv2") t]
-     ["Inductive3            indv3<C-BS>" (insert-and-expand "indv3") t]
-     ["Inductive4            indv4<C-BS>" (insert-and-expand "indv4") t]
-     ""
-     ["Section..." coq-insert-section t]
-     ""
-     ("Modules"
-      "COMMAND               ABBREVIATION"
-      ["Module (interactive)... " coq-insert-module t]
-      ["Module                mo<C-BS>" (insert-and-expand "mo") t]
-      ["Module (<:)           mo2<C-BS>" (insert-and-expand "mo") t]
-;      ["Module (interactive)  moi<C-BS>" (insert-and-expand "moi") t]
-;      ["Module (interactive <:) moi2<C-BS>" (insert-and-expand "moi2") t]
-      ["Module Type           mt<C-BS>" (insert-and-expand "mt") t]
-;      ["Module Type (interactive) mti<C-BS>" (insert-and-expand "mti") t]
-;      ""
-      ["Declare Module        dm<C-BS>" (insert-and-expand "dm") t]
-      ["Declare Module (<:)   dm2<C-BS>" (insert-and-expand "dm") t]
-;      ["Declare Module (inter.) dmi<C-BS>" (insert-and-expand "dmi") t]
-;      ["Declare Module (inter. <:) dmi2<C-BS>" (insert-and-expand "dmi2") t]
-      )
-     ("Hints"
-      "COMMAND               ABBREVIATION"
-      ["Hint Constructors     hc<C-BS>" (insert-and-expand "hc") t]
-      ["Hint Immediate        hi<C-BS>" (insert-and-expand "hi") t]
-      ["Hint Resolve          hr<C-BS>" (insert-and-expand "hr") t]
-      ["Hint Rewrite          hrw<C-BS>" (insert-and-expand "hrw") t]
-      ["Hint Extern           he<C-BS>" (insert-and-expand "he") t]
-     )
-     ("Schemes"
-      "COMMAND               ABBREVIATION"
-      ["Scheme                sc<C-BS>" (insert-and-expand "sc") t]
-      ["Functional Scheme     fs<C-BS>" (insert-and-expand "fs") t]
-      ["Functional Scheme with    fsw<C-BS>" (insert-and-expand "fsw") t]
-      )
-     ("Notations"
-      "COMMAND               ABBREVIATION"
-      ["infix                           inf<C-BS>" (insert-and-expand "inf") t]     
-      ["Notation (no assoc)             nota<C-BS>" (insert-and-expand "nota") t]     
-      ["Notation (assoc)                notas<C-BS>" (insert-and-expand "notas") t]     
-      ["Notation (no assoc, scope)      notasc<C-BS>" (insert-and-expand "notasc") t]     
-      ["Notation (assoc, scope)         notassc<C-BS>" (insert-and-expand "notassc") t]
-      )
-     )
-
-    ("Insert term" 
-     "FORM           ABBREVIATION"
-     ["forall        fo<C-BS>"  (insert-and-expand "fo") t]
-     ["forall1       fo1<C-BS>"  (insert-and-expand "fo1") t]
-     ["forall2       fo2<C-BS>" (insert-and-expand "fo2") t]
-     ["forall3       fo3<C-BS>" (insert-and-expand "fo3") t]
-     ["forall4       fo4<C-BS>" (insert-and-expand "fo4") t]
-     ""
-     ["fun           f<ctrl-bacspace>"  (insert-and-expand "f") t]
-     ["fun1          f1<ctrl-bacspace>"  (insert-and-expand "f1") t]
-     ["fun2          f2<C-BS>" (insert-and-expand "f2") t]
-     ["fun3          f3<C-BS>" (insert-and-expand "f3") t]
-     ["fun4          f4<C-BS>" (insert-and-expand "f4") t]
-     ""
-     ["if then else  if<C-BS>"  (insert-and-expand "li") t]
-     ["let in        li<C-BS>"  (insert-and-expand "li") t]
-     ""
-     ["match         m<C-BS>"  (insert-and-expand "m") t]
-     ["match2        m2<C-BS>"  (insert-and-expand "m2") t]
-     ["match3        m3<C-BS>"  (insert-and-expand "m3") t]
-     ["match4        m4<C-BS>"  (insert-and-expand "m4") t]
-     )
-
-    ("Insert tactic (a-f)" 
-     "TACTIC           ABBREVIATION"
-     ["absurd                 abs<C-BS>"  (insert-and-expand "abs") t]
-     ["assumption              as<C-BS>"  (insert-and-expand "as") t]
-     ["assert                 ass<C-BS>"  (insert-and-expand "ass") t]
-     ["auto                     a<C-BS>"  (insert-and-expand "a") t]
-     ["auto with               aw<C-BS>"  (insert-and-expand "aw") t]
-     ["auto with arith        awa<C-BS>"  (insert-and-expand "awa") t]
-     ["autorewrite             ar<C-BS>"  (insert-and-expand "ar") t]
-     ["cases                    c<C-BS>"  (insert-and-expand "c") t]
-     ["change                  ch<C-BS>"  (insert-and-expand "ch") t]
-     ["change in              chi<C-BS>"  (insert-and-expand "chi") t]
-     ["change with in        chwi<C-BS>"  (insert-and-expand "chwi") t]
-     ["constructor            con<C-BS>"  (insert-and-expand "con") t]
-     ["congruence            cong<C-BS>"  (insert-and-expand "cong") t]
-     ["decompose              dec<C-BS>"  (insert-and-expand "dec") t]
-     ["decide equality        deg<C-BS>"  (insert-and-expand "deg") t]
-     ["destruct               des<C-BS>"  (insert-and-expand "des") t]
-     ["destruct using        desu<C-BS>"  (insert-and-expand "desu") t]
-     ["destruct as           desa<C-BS>"  (insert-and-expand "desa") t]
-     ["discriminate           dis<C-BS>"  (insert-and-expand "dis") t]
-     ["eauto                   ea<C-BS>"  (insert-and-expand "ea") t]
-     ["eauto with             eaw<C-BS>"  (insert-and-expand "dec") t]
-     ["elim                     e<C-BS>"  (insert-and-expand "e") t]
-     ["elim using             elu<C-BS>"  (insert-and-expand "elu") t]
-     ["exists                  ex<C-BS>"  (insert-and-expand "ex") t]
-     ["field                  fld<C-BS>"  (insert-and-expand "fld") t]
-     ["firstorder            fsto<C-BS>"  (insert-and-expand "fsto") t]
-     ["fourier                fou<C-BS>"  (insert-and-expand "fou") t]
-     ["functional induction    fi<C-BS>"  (insert-and-expand "fi") t]
-     )
-
-    ("Insert tactic (g-z)" 
-     "TACTIC           ABBREVIATION"
-     ["generalize             g<C-BS>"  (insert-and-expand "g") t]
-     ["induction              ind<C-BS>"  (insert-and-expand "ind") t]
-     ["injection              inj<C-BS>"  (insert-and-expand "inj") t]
-     ["intro                  i<C-BS>"  (insert-and-expand "i") t]
-     ["intros                 is<C-BS>"  (insert-and-expand "is") t]
-     ["intuition              intu<C-BS>"  (insert-and-expand "intu") t]
-     ["inversion              inv<C-BS>"  (insert-and-expand "inv") t]
-     ["omega                  om<C-BS>"  (insert-and-expand "om") t]
-     ["pose                   po<C-BS>"  (insert-and-expand "om") t]
-     ["reflexivity            refl<C-BS>"  (insert-and-expand "refl") t]
-     ["replace                rep<C-BS>"  (insert-and-expand "rep") t]
-     ["rewrite                r<C-BS>"  (insert-and-expand "r") t]
-     ["rewrite in             ri<C-BS>"  (insert-and-expand "ri") t]
-     ["rewrite <-             r<<C-BS>"  (insert-and-expand "rl") t]
-     ["rewrite <- in          ri<<C-BS>"  (insert-and-expand "ril") t]
-     ["set                    set<C-BS>"  (insert-and-expand "set") t]
-     ["set in hyp             seth<C-BS>"  (insert-and-expand "seth") t]
-     ["set in goal            setg<C-BS>"  (insert-and-expand "setg") t]
-     ["set in                 seti<C-BS>"  (insert-and-expand "seti") t]
-     ["simpl                  s<C-BS>"  (insert-and-expand "s") t]
-     ["simpl                  si<C-BS>"  (insert-and-expand "si") t]
-     ["split                  sp<C-BS>"  (insert-and-expand "sp") t]
-     ["subst                  su<C-BS>"  (insert-and-expand "su") t]
-     ["symmetry               sym<C-BS>"  (insert-and-expand "sym") t]
-     ["transitivity           trans<C-BS>"  (insert-and-expand "trans") t]
-     ["trivial                t<C-BS>"  (insert-and-expand "t") t]
-     ["tauto                  ta<C-BS>"  (insert-and-expand "ta") t]
-     ["unfold                 u<C-BS>"  (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))
+ )