diff --git a/snippets/coq-mode/definitions/definition.yasnippet b/snippets/coq-mode/definitions/definition.yasnippet
new file mode 100644
index 000000000..3e4b88a00
--- /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 000000000..bac043e2c
--- /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 000000000..fb6f9b956
--- /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 000000000..60f788bc1
--- /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 000000000..e023da372
--- /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 000000000..5db7e7520
--- /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 000000000..378e32457
--- /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 000000000..58a7b08cb
--- /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 000000000..1380fe624
--- /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 000000000..5c588d49f
--- /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 000000000..0b5bdff7c
--- /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 000000000..ccbd68bfb
--- /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 000000000..ce66014ce
--- /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 000000000..8998223d9
--- /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 000000000..f678f0b88
--- /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 000000000..4c7270ce3
--- /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 000000000..096a63c03
--- /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 000000000..6bf9aaca2
--- /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 000000000..8c60db58f
--- /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 000000000..10cb1f744
--- /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 000000000..fefb8bab9
--- /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 000000000..8cf2e7696
--- /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 000000000..2dcf18ef7
--- /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 000000000..b8e721d6f
--- /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 000000000..92f8a4543
--- /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 000000000..47ee34803
--- /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 000000000..4d624aa8a
--- /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 000000000..4d74992df
--- /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 000000000..3b6a36569
--- /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 000000000..4dedb7f74
--- /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 000000000..ad03a0fa9
--- /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 000000000..cedd12dc0
--- /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 000000000..435b84552
--- /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 000000000..f13e03e00
--- /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 000000000..4b26f462a
--- /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 000000000..5c1805249
--- /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 000000000..e259b8936
--- /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 000000000..25a83ba6f
--- /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 000000000..aa27b246c
--- /dev/null
+++ b/snippets/coq-mode/tactics/rewrite.yasnippet
@@ -0,0 +1,6 @@
+# -*- mode: snippet -*-
+# key: rw
+# group: tactics
+# name: rewrite
+# --
+rewrite $0.