added some lines in holes short doc. And some abbrevs for coq.

1 files changed, 40 insertions, 24 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 5c728dab..baad752c 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -25,21 +25,19 @@
 		  ("i" "intro" nil 0)
 		  ("h" "Hints  : ." nil 0)
 		  ("g" "generalize" nil 0)
-		  ("co" "constructor" nil 0)
+		  ("con" "constructor" nil 0)
 		  ("e" "elim" nil 0)
-		  ("c" "constructor" nil 0)
 		  ("ge" "generalize" nil 0)
 		  ("sym" "symmetry" nil 0)
 		  ("a" "auto" nil 0)
 		  ("re" "rewrite" nil 0)
-		  ("eawa" "eauto with acthint" nil 0)
+		  ("eawa" "eauto with arith" nil 0)
 		  ("un" "unfold" nil 0)
 		  ("eaw" "eauto with" nil 0)
 		  ("f" "forall #:#,#" nil 0)
 		  ("fi" "functional induction" nil 0)
 		  ("fs" "Functional Scheme xxx := Induction for yyy (opt:with ...)." nil 0)
 		  ("sc" "Scheme := Induction for Sort ." nil 0)
-		  ("fi" "Fixpoint ." nil 0)
 		  ("f" "fun (:) => " nil 0)
 		  ("eap" "eapply" nil 0)
 		  ("ex" "exists" nil 0)
@@ -54,14 +52,12 @@
 		  ("au" "auto" nil 0)
 		  ("as" "assumption" nil 0)
 		  ("sy" "symmetry" nil 0)
-		  ("ar" "auto with arith" nil 0)
 		  ("el" "elim" nil 0)
 		  ("ap" "apply" nil 0)
 		  ("gen" "generalize" nil 0)
 		  ("hr" "Hint Resolve :." nil 0)
 		  ("ind" "induction" nil 0)
-		  ("fix" "Fixpoint # (# : #) {struct #} : # := #." nil 0)
-		  ("sp" "simpl" nil 0)
+		  ("fix" "Fixpoint X (X : X) {struct X} : X := X." nil 0)
 		  ("re<" "rewrite <-" nil 0)
 		  ("ea" "eauto" nil 0)
 		  ("def" "Definition : :=." nil 0)
@@ -69,19 +65,25 @@
   (define-abbrev-table 'coq-mode-abbrev-table
 	 '(
 		("m" "match # with 
-#" holes-abbrev-complete 1)
+# => #" holes-abbrev-complete 1)
 		("m|" "match # with 
- #
-|#" holes-abbrev-complete 1)
+ # => #
+| # => #" holes-abbrev-complete 1)
 		("m||" "match # with 
- #
-|#
-|#" holes-abbrev-complete 1)
+  # => #
+| # => #
+| # => #" holes-abbrev-complete 1)
 		("m|||" "match # with 
- #
-|#
-|#
-|#" holes-abbrev-complete 1)
+  # => #
+| # => #
+| # => #
+| # => #" holes-abbrev-complete 1)
+		("m||||" "match # with 
+  # => #
+| # => #
+| # => #
+| # => #
+| # => #" holes-abbrev-complete 1)
 		("c" "cases #" holes-abbrev-complete 1)
 		("u" "unfold #" holes-abbrev-complete 1)
 		("si" "simpl" holes-abbrev-complete 0)
@@ -94,7 +96,25 @@
 		("r" "rewrite #" holes-abbrev-complete 19)
 		("di" "discriminate" holes-abbrev-complete 0)
 		("p" "Print #" holes-abbrev-complete 3)
-		("indv" "Inductive #" holes-abbrev-complete 0)
+		("indv" "Inductive # : # := #." holes-abbrev-complete 0)
+		("indv|" "Inductive # : # :=
+  # : #
+| # : #." holes-abbrev-complete 0)
+		("indv||" "Inductive # : # :=
+  # : #
+| # : #
+| # : #." holes-abbrev-complete 0)
+		("indv|||" "Inductive # : # :=
+  # : #
+| # : #
+| # : #
+| # : #." holes-abbrev-complete 0)
+		("indv||||" "Inductive # : # :=
+  # : #
+| # : #
+| # : #
+| # : #
+| # : #." holes-abbrev-complete 0)
 		("o" "abstract omega" holes-abbrev-complete 0)
 		("l" "Lemma # : #." holes-abbrev-complete 4)
 		("awa" "auto with arith" holes-abbrev-complete 4)
@@ -111,14 +131,13 @@
 		("f::" "fun (#:#) (#:#) => #" holes-abbrev-complete 0)
 		("f:::" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
 		("f::::" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
-		("co" "constructor" holes-abbrev-complete 0)
 		("e" "elim #" holes-abbrev-complete 1)
-		("c" "constructor" holes-abbrev-complete 3)
+		("con" "constructor" holes-abbrev-complete 3)
 		("ge" "generalize #" holes-abbrev-complete 0)
 		("sym" "symmetry" holes-abbrev-complete 0)
 		("a" "auto" holes-abbrev-complete 4)
 		("re" "rewrite #" holes-abbrev-complete 0)
-		("eawa" "eauto with acthint" holes-abbrev-complete 0)
+		("eawa" "eauto with arith" holes-abbrev-complete 0)
 		("un" "unfold #" holes-abbrev-complete 7)
 		("eaw" "eauto with #" holes-abbrev-complete 0)
 		("fi" "functional induction #" holes-abbrev-complete 0)
@@ -127,7 +146,6 @@
 		("fsw" "Functional Scheme # := Induction for # with #." 
 		 holes-abbrev-complete 0)
 		("sc" "Scheme # := Induction for # Sort #." nil 0)
-		("invf" "Invfunproof # params #." holes-abbrev-complete 0)
 		("eap" "eapply #" holes-abbrev-complete 0)
 		("ex" "exists #" holes-abbrev-complete 0)
 		("inv" "inversion #" holes-abbrev-complete 9)
@@ -141,14 +159,12 @@
 		("au" "auto" holes-abbrev-complete 1)
 		("as" "assumption" holes-abbrev-complete 4)
 		("sy" "symmetry" holes-abbrev-complete 0)
-		("ar" "auto with arith" holes-abbrev-complete 0)
 		("el" "elim #" holes-abbrev-complete 0)
 		("ap" "apply #" holes-abbrev-complete 16)
 		("gen" "generalize #" holes-abbrev-complete 0)
 		("hr" "Hint Resolve : #." holes-abbrev-complete 0)
 		("ind" "induction #" holes-abbrev-complete 2)
 		("fix" "Fixpoint # (#:#) {struct #} : # :=" holes-abbrev-complete 3)
-		("sp" "simpl" holes-abbrev-complete 2)
 		("re<" "rewrite <- #" holes-abbrev-complete 0)
 		("ea" "eauto" holes-abbrev-complete 0)
 		("def" "Definition #:# := #." holes-abbrev-complete 5)