diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 47 | ||||
| -rw-r--r-- | coq/coq.el | 71 |
2 files changed, 66 insertions, 52 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 6d9a097e..15302aeb 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -10,28 +10,28 @@ (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) + ("ar" "autorewrite [ # ] using @{db}" 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) + ("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) + ("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) + ("dec" "decompose [#] @{hyp}" 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) ("deg" "decide equality" holes-abbrev-complete 3) - ("des" "destruct #" holes-abbrev-complete 0) + ("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) @@ -42,7 +42,7 @@ ("e" "elim #" holes-abbrev-complete 1) ("ea" "eauto" holes-abbrev-complete 0) ("eap" "eapply #" holes-abbrev-complete 0) - ("eaw" "eauto with #" 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) @@ -52,30 +52,30 @@ ("f2" "fun (#:#) (#:#) => #" holes-abbrev-complete 0) ("f3" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) ("f4" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) - ("fi" "functional induction #" holes-abbrev-complete 0) - ("fix" "Fixpoint # (#:#) {struct #} : # :=\n#." holes-abbrev-complete 3) + ("fi" "functional induction @{f} @{args}" holes-abbrev-complete 0) + ("fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." holes-abbrev-complete 3) ("fo" "forall #,#" holes-abbrev-complete 0) ("fo1" "forall #:#,#" holes-abbrev-complete 0) ("fo2" "forall (#:#) (#:#), #" holes-abbrev-complete 0) ("fo3" "forall (#:#) (#:#) (#:#), #" holes-abbrev-complete 0) ("fo4" "forall (#:#) (#:#) (#:#) (#:#), #" holes-abbrev-complete 0) - ("fs" "Functional Scheme # := Induction for #." holes-abbrev-complete 0) + ("fs" "Functional Scheme @{name} := Induction for @{fun}." holes-abbrev-complete 0) ("fsto" "firstorder" holes-abbrev-complete 0) - ("fsw" "Functional Scheme # := Induction for # with #." holes-abbrev-complete 0) + ("fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." holes-abbrev-complete 0) ("g" "generalize #" holes-abbrev-complete 0) ("ge" "generalize #" holes-abbrev-complete 0) ("gen" "generalize #" 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) - ("hrw" "Hint Rewrite [#] in # using #." holes-abbrev-complete 0) + ("he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." holes-abbrev-complete 0) + ("hi" "Hint Immediate # : @{db}." holes-abbrev-complete 0) + ("hr" "Hint Resolve # : @{db}." holes-abbrev-complete 0) + ("hrw" "Hint Rewrite [#] in @{db} using @{tac}." holes-abbrev-complete 0) ("hs" "Hints # : #." holes-abbrev-complete 0) ("hu" "Hint Unfold # : #." holes-abbrev-complete 0) - ("i" "intro #" holes-abbrev-complete 10) + ("i" "intro " holes-abbrev-complete 10) ("if" "if # then # else #" holes-abbrev-complete 1) ("in" "intro" holes-abbrev-complete 1) - ("inf" "infix \"#\" := # (at level #) : #." holes-abbrev-complete 1) + ("inf" "infix \"#\" := # (at level #) : @{scope}." holes-abbrev-complete 1) ("ind" "induction #" holes-abbrev-complete 2) ("indv" "Inductive # : # := # : #." holes-abbrev-complete 0) ("indv2" "Inductive # : # :=\n| # : #\n| # : #." holes-abbrev-complete 0) @@ -102,8 +102,8 @@ ("moi2" "Module # <: #.\n#\nEnd #." holes-abbrev-complete 0) ("nota" "Notation \"#\" := # (at level #, # at level #)." holes-abbrev-complete 0) ("notas" "Notation \"#\" := # (at level #, # associativity)." holes-abbrev-complete 0) - ("notasc" "Notation \"#\" := # (at level #, # at level #) : #." holes-abbrev-complete 0) - ("notassc" "Notation \"#\" := # (at level #, # associativity) : #." holes-abbrev-complete 0) + ("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) ("p" "Print #" holes-abbrev-complete 3) @@ -116,6 +116,7 @@ ("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) @@ -125,7 +126,7 @@ ("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) + ("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) @@ -101,32 +101,42 @@ ["Inductive3 indv3<C-BS>" (insert-and-expand "indv3") t] ["Inductive4 indv4<C-BS>" (insert-and-expand "indv4") 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] - "" - ["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] - "" - ["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] - "" - ["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] + ("Modules" + "COMMAND ABBREVIATION" + ["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" @@ -136,13 +146,16 @@ ["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] @@ -195,9 +208,9 @@ ["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 "r") t] - ["rewrite <- rl<C-BS>" (insert-and-expand "r") t] - ["rewrite <- in ril<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] |