From 2eac2f8b6fbf2670f14770cf00518fe65716129d Mon Sep 17 00:00:00 2001
From: Peter Urbak <pu@opentelehealth.com>
Date: Sun, 6 Oct 2019 22:09:59 +0200
Subject: [PATCH] Adds snippets for coq-mode

---
 snippets/coq-mode/definitions/definition.yasnippet    |  7 +++++++
 snippets/coq-mode/definitions/fixpoint-with.yasnippet |  9 +++++++++
 snippets/coq-mode/definitions/fixpoint.yasnippet      |  7 +++++++
 snippets/coq-mode/definitions/fun.yasnippet           |  6 ++++++
 snippets/coq-mode/definitions/inductive.yasnippet     |  8 ++++++++
 snippets/coq-mode/lookup/check.yasnippet              |  7 +++++++
 snippets/coq-mode/lookup/locate.yasnippet             |  7 +++++++
 snippets/coq-mode/lookup/print.yasnippet              |  7 +++++++
 snippets/coq-mode/lookup/search.yasnippet             |  7 +++++++
 snippets/coq-mode/lookup/searchabout.yasnippet        |  7 +++++++
 snippets/coq-mode/lookup/searchpattern.yasnippet      |  7 +++++++
 snippets/coq-mode/misc/forall.yasnippet               |  6 ++++++
 snippets/coq-mode/misc/if.yasnippet                   |  6 ++++++
 snippets/coq-mode/misc/infix.yasnippet                |  7 +++++++
 snippets/coq-mode/misc/match.yasnippet                |  8 ++++++++
 snippets/coq-mode/misc/notation.yasnippet             |  7 +++++++
 snippets/coq-mode/misc/require.yasnippet              |  7 +++++++
 snippets/coq-mode/propositions/axiom.yasnippet        |  8 ++++++++
 snippets/coq-mode/propositions/conjecture.yasnippet   |  6 ++++++
 snippets/coq-mode/propositions/corollary.yasnippet    | 11 +++++++++++
 snippets/coq-mode/propositions/example.yasnippet      | 11 +++++++++++
 snippets/coq-mode/propositions/fact.yasnippet         | 11 +++++++++++
 snippets/coq-mode/propositions/hypotheses.yasnippet   |  6 ++++++
 snippets/coq-mode/propositions/hypothesis.yasnippet   |  6 ++++++
 snippets/coq-mode/propositions/instance.yasnippet     | 11 +++++++++++
 snippets/coq-mode/propositions/lemma.yasnippet        | 11 +++++++++++
 snippets/coq-mode/propositions/parameter.yasnippet    |  6 ++++++
 snippets/coq-mode/propositions/proposition.yasnippet  | 11 +++++++++++
 snippets/coq-mode/propositions/remark.yasnippet       | 11 +++++++++++
 snippets/coq-mode/propositions/theorem.yasnippet      | 11 +++++++++++
 snippets/coq-mode/propositions/variable.yasnippet     |  6 ++++++
 snippets/coq-mode/propositions/variables.yasnippet    |  6 ++++++
 snippets/coq-mode/tactics/case.yasnippet              |  6 ++++++
 snippets/coq-mode/tactics/destruct.yasnippet          |  6 ++++++
 snippets/coq-mode/tactics/induction.yasnippet         |  6 ++++++
 snippets/coq-mode/tactics/rename.yasnippet            |  7 +++++++
 snippets/coq-mode/tactics/rewrite-left.yasnippet      |  6 ++++++
 snippets/coq-mode/tactics/rewrite-right.yasnippet     |  6 ++++++
 snippets/coq-mode/tactics/rewrite.yasnippet           |  6 ++++++
 39 files changed, 295 insertions(+)
 create mode 100644 snippets/coq-mode/definitions/definition.yasnippet
 create mode 100644 snippets/coq-mode/definitions/fixpoint-with.yasnippet
 create mode 100644 snippets/coq-mode/definitions/fixpoint.yasnippet
 create mode 100644 snippets/coq-mode/definitions/fun.yasnippet
 create mode 100644 snippets/coq-mode/definitions/inductive.yasnippet
 create mode 100644 snippets/coq-mode/lookup/check.yasnippet
 create mode 100644 snippets/coq-mode/lookup/locate.yasnippet
 create mode 100644 snippets/coq-mode/lookup/print.yasnippet
 create mode 100644 snippets/coq-mode/lookup/search.yasnippet
 create mode 100644 snippets/coq-mode/lookup/searchabout.yasnippet
 create mode 100644 snippets/coq-mode/lookup/searchpattern.yasnippet
 create mode 100644 snippets/coq-mode/misc/forall.yasnippet
 create mode 100644 snippets/coq-mode/misc/if.yasnippet
 create mode 100644 snippets/coq-mode/misc/infix.yasnippet
 create mode 100644 snippets/coq-mode/misc/match.yasnippet
 create mode 100644 snippets/coq-mode/misc/notation.yasnippet
 create mode 100644 snippets/coq-mode/misc/require.yasnippet
 create mode 100644 snippets/coq-mode/propositions/axiom.yasnippet
 create mode 100644 snippets/coq-mode/propositions/conjecture.yasnippet
 create mode 100644 snippets/coq-mode/propositions/corollary.yasnippet
 create mode 100644 snippets/coq-mode/propositions/example.yasnippet
 create mode 100644 snippets/coq-mode/propositions/fact.yasnippet
 create mode 100644 snippets/coq-mode/propositions/hypotheses.yasnippet
 create mode 100644 snippets/coq-mode/propositions/hypothesis.yasnippet
 create mode 100644 snippets/coq-mode/propositions/instance.yasnippet
 create mode 100644 snippets/coq-mode/propositions/lemma.yasnippet
 create mode 100644 snippets/coq-mode/propositions/parameter.yasnippet
 create mode 100644 snippets/coq-mode/propositions/proposition.yasnippet
 create mode 100644 snippets/coq-mode/propositions/remark.yasnippet
 create mode 100644 snippets/coq-mode/propositions/theorem.yasnippet
 create mode 100644 snippets/coq-mode/propositions/variable.yasnippet
 create mode 100644 snippets/coq-mode/propositions/variables.yasnippet
 create mode 100644 snippets/coq-mode/tactics/case.yasnippet
 create mode 100644 snippets/coq-mode/tactics/destruct.yasnippet
 create mode 100644 snippets/coq-mode/tactics/induction.yasnippet
 create mode 100644 snippets/coq-mode/tactics/rename.yasnippet
 create mode 100644 snippets/coq-mode/tactics/rewrite-left.yasnippet
 create mode 100644 snippets/coq-mode/tactics/rewrite-right.yasnippet
 create mode 100644 snippets/coq-mode/tactics/rewrite.yasnippet

diff --git a/snippets/coq-mode/definitions/definition.yasnippet b/snippets/coq-mode/definitions/definition.yasnippet
new file mode 100644
index 0000000..3e4b88a
--- /dev/null
+++ b/snippets/coq-mode/definitions/definition.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: Def
+# group: definitions
+# name: Definition
+# --
+Definition $1 ($2 : $3) : $4 :=
+  $0.
diff --git a/snippets/coq-mode/definitions/fixpoint-with.yasnippet b/snippets/coq-mode/definitions/fixpoint-with.yasnippet
new file mode 100644
index 0000000..bac043e
--- /dev/null
+++ b/snippets/coq-mode/definitions/fixpoint-with.yasnippet
@@ -0,0 +1,9 @@
+# -*- mode: snippet -*-
+# key: Fixpw
+# group: definitions
+# name: Fixpoint-with
+# --
+Fixpoint $1 ($2 : $3) : $4 :=
+  $9
+with $5 ($6 : $7) : $8 :=
+  $0.
\ No newline at end of file
diff --git a/snippets/coq-mode/definitions/fixpoint.yasnippet b/snippets/coq-mode/definitions/fixpoint.yasnippet
new file mode 100644
index 0000000..fb6f9b9
--- /dev/null
+++ b/snippets/coq-mode/definitions/fixpoint.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: Fixp
+# group: definitions
+# name: Fixpoint
+# --
+Fixpoint $1 ($2 : $3) : $4 :=
+  $0.
\ No newline at end of file
diff --git a/snippets/coq-mode/definitions/fun.yasnippet b/snippets/coq-mode/definitions/fun.yasnippet
new file mode 100644
index 0000000..60f788b
--- /dev/null
+++ b/snippets/coq-mode/definitions/fun.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: fun
+# group: definitions
+# name: fun
+# --
+fun ($1 : $2 => $0)
diff --git a/snippets/coq-mode/definitions/inductive.yasnippet b/snippets/coq-mode/definitions/inductive.yasnippet
new file mode 100644
index 0000000..e023da3
--- /dev/null
+++ b/snippets/coq-mode/definitions/inductive.yasnippet
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# key: Ind
+# group: definitions
+# name: Inductive
+# --
+Inductive $1 : $2 :=
+| $0
+.
diff --git a/snippets/coq-mode/lookup/check.yasnippet b/snippets/coq-mode/lookup/check.yasnippet
new file mode 100644
index 0000000..5db7e75
--- /dev/null
+++ b/snippets/coq-mode/lookup/check.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: C
+# group: lookup
+# name: Check
+# --
+Check $1.
+$0
diff --git a/snippets/coq-mode/lookup/locate.yasnippet b/snippets/coq-mode/lookup/locate.yasnippet
new file mode 100644
index 0000000..378e324
--- /dev/null
+++ b/snippets/coq-mode/lookup/locate.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: L
+# group: lookup
+# name: Locate
+# --
+Locate "$1".
+$0
diff --git a/snippets/coq-mode/lookup/print.yasnippet b/snippets/coq-mode/lookup/print.yasnippet
new file mode 100644
index 0000000..58a7b08
--- /dev/null
+++ b/snippets/coq-mode/lookup/print.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: P
+# group: lookup
+# name: Print
+# --
+Print $1.
+$0
diff --git a/snippets/coq-mode/lookup/search.yasnippet b/snippets/coq-mode/lookup/search.yasnippet
new file mode 100644
index 0000000..1380fe6
--- /dev/null
+++ b/snippets/coq-mode/lookup/search.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: S
+# group: lookup
+# name: Search
+# --
+Search $1.
+$0
diff --git a/snippets/coq-mode/lookup/searchabout.yasnippet b/snippets/coq-mode/lookup/searchabout.yasnippet
new file mode 100644
index 0000000..5c588d4
--- /dev/null
+++ b/snippets/coq-mode/lookup/searchabout.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: SA
+# group: lookup
+# name: SearchAbout
+# --
+SearchAbout $1.
+$0
diff --git a/snippets/coq-mode/lookup/searchpattern.yasnippet b/snippets/coq-mode/lookup/searchpattern.yasnippet
new file mode 100644
index 0000000..0b5bdff
--- /dev/null
+++ b/snippets/coq-mode/lookup/searchpattern.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: SP
+# group: lookup
+# name: SearchPattern
+# --
+SearchPattern ($1).
+$0
diff --git a/snippets/coq-mode/misc/forall.yasnippet b/snippets/coq-mode/misc/forall.yasnippet
new file mode 100644
index 0000000..ccbd68b
--- /dev/null
+++ b/snippets/coq-mode/misc/forall.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: fa
+# group: misc
+# name: forall
+# --
+forall ($1 : $2), $0
diff --git a/snippets/coq-mode/misc/if.yasnippet b/snippets/coq-mode/misc/if.yasnippet
new file mode 100644
index 0000000..ce66014
--- /dev/null
+++ b/snippets/coq-mode/misc/if.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: if
+# group: misc
+# name: if
+# --
+if $1 then $2 else $0
diff --git a/snippets/coq-mode/misc/infix.yasnippet b/snippets/coq-mode/misc/infix.yasnippet
new file mode 100644
index 0000000..8998223
--- /dev/null
+++ b/snippets/coq-mode/misc/infix.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: Inf
+# group: misc
+# name: Infix
+# --
+Infix "$1" := $2 (at level $3, $4 associativity).
+$0
diff --git a/snippets/coq-mode/misc/match.yasnippet b/snippets/coq-mode/misc/match.yasnippet
new file mode 100644
index 0000000..f678f0b
--- /dev/null
+++ b/snippets/coq-mode/misc/match.yasnippet
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# key: match
+# group: misc
+# name: match
+# --
+match $1 with
+  | $0 =>
+end
\ No newline at end of file
diff --git a/snippets/coq-mode/misc/notation.yasnippet b/snippets/coq-mode/misc/notation.yasnippet
new file mode 100644
index 0000000..4c7270c
--- /dev/null
+++ b/snippets/coq-mode/misc/notation.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: Nota
+# group: misc
+# name: Notation
+# --
+Notation "$1" := ($2) (at level $3, $4 associativity).
+$0
diff --git a/snippets/coq-mode/misc/require.yasnippet b/snippets/coq-mode/misc/require.yasnippet
new file mode 100644
index 0000000..096a63c
--- /dev/null
+++ b/snippets/coq-mode/misc/require.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: Req
+# group: misc
+# name: Require
+# --
+${1:$$(coq-insert-requires)}
+$0
\ No newline at end of file
diff --git a/snippets/coq-mode/propositions/axiom.yasnippet b/snippets/coq-mode/propositions/axiom.yasnippet
new file mode 100644
index 0000000..6bf9aac
--- /dev/null
+++ b/snippets/coq-mode/propositions/axiom.yasnippet
@@ -0,0 +1,8 @@
+# -*- mode: snippet -*-
+# key: Axi
+# group: propositions
+# name: Axiom
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Axiom $1 :
+  $0.
diff --git a/snippets/coq-mode/propositions/conjecture.yasnippet b/snippets/coq-mode/propositions/conjecture.yasnippet
new file mode 100644
index 0000000..8c60db5
--- /dev/null
+++ b/snippets/coq-mode/propositions/conjecture.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: Conj
+# group: propositions
+# name: Conjecture
+# --
+Conjecture $1 : $0.
diff --git a/snippets/coq-mode/propositions/corollary.yasnippet b/snippets/coq-mode/propositions/corollary.yasnippet
new file mode 100644
index 0000000..10cb1f7
--- /dev/null
+++ b/snippets/coq-mode/propositions/corollary.yasnippet
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: Cor
+# group: propositions
+# name: Corollary
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Corollary $1 :
+  $2.
+Proof.
+  $0
+Qed.
diff --git a/snippets/coq-mode/propositions/example.yasnippet b/snippets/coq-mode/propositions/example.yasnippet
new file mode 100644
index 0000000..fefb8ba
--- /dev/null
+++ b/snippets/coq-mode/propositions/example.yasnippet
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: Exp
+# group: propositions
+# name: Example
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Example $1 :
+  $2.
+Proof.
+  $0
+Qed.
diff --git a/snippets/coq-mode/propositions/fact.yasnippet b/snippets/coq-mode/propositions/fact.yasnippet
new file mode 100644
index 0000000..8cf2e76
--- /dev/null
+++ b/snippets/coq-mode/propositions/fact.yasnippet
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: Fact
+# group: propositions
+# name: Fact
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Fact $1 :
+  $2.
+Proof.
+  $0
+Qed.
diff --git a/snippets/coq-mode/propositions/hypotheses.yasnippet b/snippets/coq-mode/propositions/hypotheses.yasnippet
new file mode 100644
index 0000000..2dcf18e
--- /dev/null
+++ b/snippets/coq-mode/propositions/hypotheses.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: Hypos
+# group: propositions
+# name: Hypotheses
+# --
+Hypotheses $1 : $0.
diff --git a/snippets/coq-mode/propositions/hypothesis.yasnippet b/snippets/coq-mode/propositions/hypothesis.yasnippet
new file mode 100644
index 0000000..b8e721d
--- /dev/null
+++ b/snippets/coq-mode/propositions/hypothesis.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: Hypo
+# group: propositions
+# name: Hypothesis
+# --
+Hypothesis $1 : $0.
diff --git a/snippets/coq-mode/propositions/instance.yasnippet b/snippets/coq-mode/propositions/instance.yasnippet
new file mode 100644
index 0000000..92f8a45
--- /dev/null
+++ b/snippets/coq-mode/propositions/instance.yasnippet
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: Ins
+# group: propositions
+# name: Instance
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Instance $1 :
+  $2.
+Proof.
+  $0
+Qed.
diff --git a/snippets/coq-mode/propositions/lemma.yasnippet b/snippets/coq-mode/propositions/lemma.yasnippet
new file mode 100644
index 0000000..47ee348
--- /dev/null
+++ b/snippets/coq-mode/propositions/lemma.yasnippet
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: Lem
+# group: propositions
+# name: Lemma
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Lemma $1 :
+  $2.
+Proof.
+  $0
+Qed.
diff --git a/snippets/coq-mode/propositions/parameter.yasnippet b/snippets/coq-mode/propositions/parameter.yasnippet
new file mode 100644
index 0000000..4d624aa
--- /dev/null
+++ b/snippets/coq-mode/propositions/parameter.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: Param
+# group: propositions
+# name: Parameters
+# --
+Parameter $1 : $0.
diff --git a/snippets/coq-mode/propositions/proposition.yasnippet b/snippets/coq-mode/propositions/proposition.yasnippet
new file mode 100644
index 0000000..4d74992
--- /dev/null
+++ b/snippets/coq-mode/propositions/proposition.yasnippet
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: Pro
+# group: propositions
+# name: Proposition
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Proposition $1 :
+  $2.
+Proof.
+  $0
+Qed.
diff --git a/snippets/coq-mode/propositions/remark.yasnippet b/snippets/coq-mode/propositions/remark.yasnippet
new file mode 100644
index 0000000..3b6a365
--- /dev/null
+++ b/snippets/coq-mode/propositions/remark.yasnippet
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: Rem
+# group: propositions
+# name: Remark
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Remark $1 :
+  $2.
+Proof.
+  $0
+Qed.
diff --git a/snippets/coq-mode/propositions/theorem.yasnippet b/snippets/coq-mode/propositions/theorem.yasnippet
new file mode 100644
index 0000000..4dedb7f
--- /dev/null
+++ b/snippets/coq-mode/propositions/theorem.yasnippet
@@ -0,0 +1,11 @@
+# -*- mode: snippet -*-
+# key: The
+# group: propositions
+# name: Theorem
+# expand-env: ((yas-indent-line 'fixed))
+# --
+Theorem $1 :
+  $2.
+Proof.
+  $0
+Qed.
\ No newline at end of file
diff --git a/snippets/coq-mode/propositions/variable.yasnippet b/snippets/coq-mode/propositions/variable.yasnippet
new file mode 100644
index 0000000..ad03a0f
--- /dev/null
+++ b/snippets/coq-mode/propositions/variable.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: Var
+# group: propositions
+# name: Variable
+# --
+Variable $1 : $0.
diff --git a/snippets/coq-mode/propositions/variables.yasnippet b/snippets/coq-mode/propositions/variables.yasnippet
new file mode 100644
index 0000000..cedd12d
--- /dev/null
+++ b/snippets/coq-mode/propositions/variables.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: Vars
+# group: propositions
+# name: Variables
+# --
+Variables $1 : $0.
diff --git a/snippets/coq-mode/tactics/case.yasnippet b/snippets/coq-mode/tactics/case.yasnippet
new file mode 100644
index 0000000..435b845
--- /dev/null
+++ b/snippets/coq-mode/tactics/case.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: case
+# group: tactics
+# name: case
+# --
+case ${1:n} as [ | $1' ].$0
diff --git a/snippets/coq-mode/tactics/destruct.yasnippet b/snippets/coq-mode/tactics/destruct.yasnippet
new file mode 100644
index 0000000..f13e03e
--- /dev/null
+++ b/snippets/coq-mode/tactics/destruct.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: des
+# group: tactics
+# name: destruct
+# --
+destruct $1 as [ $0 ].
\ No newline at end of file
diff --git a/snippets/coq-mode/tactics/induction.yasnippet b/snippets/coq-mode/tactics/induction.yasnippet
new file mode 100644
index 0000000..4b26f46
--- /dev/null
+++ b/snippets/coq-mode/tactics/induction.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: ind
+# group: tactics
+# name: induction
+# --
+induction ${1:n} as [ | $1' IH_$1' ].$0
\ No newline at end of file
diff --git a/snippets/coq-mode/tactics/rename.yasnippet b/snippets/coq-mode/tactics/rename.yasnippet
new file mode 100644
index 0000000..5c18052
--- /dev/null
+++ b/snippets/coq-mode/tactics/rename.yasnippet
@@ -0,0 +1,7 @@
+# -*- mode: snippet -*-
+# key: rename
+# group: tactics
+# name: rename
+# --
+rename $1 into $2.
+$0
\ No newline at end of file
diff --git a/snippets/coq-mode/tactics/rewrite-left.yasnippet b/snippets/coq-mode/tactics/rewrite-left.yasnippet
new file mode 100644
index 0000000..e259b89
--- /dev/null
+++ b/snippets/coq-mode/tactics/rewrite-left.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: rwl
+# group: tactics
+# name: rewrite-left
+# --
+rewrite <- $0.
diff --git a/snippets/coq-mode/tactics/rewrite-right.yasnippet b/snippets/coq-mode/tactics/rewrite-right.yasnippet
new file mode 100644
index 0000000..25a83ba
--- /dev/null
+++ b/snippets/coq-mode/tactics/rewrite-right.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: rwr
+# group: tactics
+# name: rewrite-right
+# --
+rewrite -> $0.
diff --git a/snippets/coq-mode/tactics/rewrite.yasnippet b/snippets/coq-mode/tactics/rewrite.yasnippet
new file mode 100644
index 0000000..aa27b24
--- /dev/null
+++ b/snippets/coq-mode/tactics/rewrite.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: rw
+# group: tactics
+# name: rewrite
+# --
+rewrite $0.