;; 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) ;#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 [ # ] 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) ("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 #" 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" "fun # => #" holes-abbrev-complete 0) ("f1" "fun #:# => #" holes-abbrev-complete 0) ("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) ("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) ("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) ("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) ("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) ("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) ("m" "match # with\n# => #\nend" holes-abbrev-complete 1) ("m2" "match # with\n # => #\n| # => #\nend" holes-abbrev-complete 1) ("m3" "match # with\n # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1) ("m4" "match # with\n# => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1) ("m5" "match # with\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) ("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 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) ) ) )