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-abbrev-V7.el | 262 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 262 insertions(+) create mode 100644 coq/coq-abbrev-V7.el (limited to 'coq/coq-abbrev-V7.el') 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" (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] + ) + ) + + ("Insert term" + "FORM ABBREVIATION" + ["forall fo" (insert-and-expand "fo") t] + "" + ["fun f" (insert-and-expand "f") t] + "" + ["let in li" (insert-and-expand "li") t] + "" + ["Cases c" (insert-and-expand "c") t] + ["Cases2 c2" (insert-and-expand "c2") t] + ["Cases3 c3" (insert-and-expand "c3") t] + ["Cases4 c4" (insert-and-expand "c4") 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] + ) + + ("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] + ["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] )) + +(provide 'coq-abbrev-V7) + -- cgit v1.2.3