diff --git a/rc/filetype/coq.kak b/rc/filetype/coq.kak
index 265bc94e..6fbc0998 100644
--- a/rc/filetype/coq.kak
+++ b/rc/filetype/coq.kak
@@ -27,81 +27,81 @@ provide-module coq %{
 # Syntax
 # ------
 
-    # This is a `looks sensible' keyword syntax highlighting, far from being correct.
-    # Note that only the core language and the proof language is supported,
-    # the Ltac language is not (for now).
+# This is a `looks sensible' keyword syntax highlighting, far from being correct.
+# Note that only the core language and the proof language is supported,
+# the Ltac language is not (for now).
      
-    add-highlighter shared/coq regions
+add-highlighter shared/coq regions
 
-    add-highlighter shared/coq/comment region -recurse \Q(* \Q(* \Q*) fill comment
-    add-highlighter shared/coq/string region (?<!")" (?<!")("")*" fill string
+add-highlighter shared/coq/comment region -recurse \Q(* \Q(* \Q*) fill comment
+add-highlighter shared/coq/string region (?<!")" (?<!")("")*" fill string
 
-    add-highlighter shared/coq/command default-region group
+add-highlighter shared/coq/command default-region group
 
-    # This is not any lexical convention of coq, simply highlighting used to make
-    # proofs look better, based on how people usually use notations
-    add-highlighter shared/coq/command/ regex [`!@#$%^&*-=+\\:\;|<>/]+ 0:operator
-    add-highlighter shared/coq/command/ regex \(dfs\)|\(bfs\)          0:operator
-    add-highlighter shared/coq/command/ regex [()\[\]{}]               0:operator
+# This is not any lexical convention of coq, simply highlighting used to make
+# proofs look better, based on how people usually use notations
+add-highlighter shared/coq/command/ regex [`!@#$%^&*-=+\\:\;|<>/]+ 0:operator
+add-highlighter shared/coq/command/ regex \(dfs\)|\(bfs\)          0:operator
+add-highlighter shared/coq/command/ regex [()\[\]{}]               0:operator
 
-    # numeral literals
-    add-highlighter shared/coq/command/ regex [-]?[0-9][0-9_]*(\.[0-9_]+)?([eE][+-][0-9_]+)? 0:value
+# numeral literals
+add-highlighter shared/coq/command/ regex [-]?[0-9][0-9_]*(\.[0-9_]+)?([eE][+-][0-9_]+)? 0:value
 
-    evaluate-commands %sh{
-        # These are builtin keywords of the Gallina language (without tactics)
-        keywords="_ IF Prop SProp Set Type as at by cofix discriminated else end exists exists2 fix for"
-        keywords="${keywords} forall fun if in lazymatch let match multimatch return then using where with"
-        keywords="${keywords} inside outside"
+evaluate-commands %sh{
+    # These are builtin keywords of the Gallina language (without tactics)
+    keywords="_ IF Prop SProp Set Type as at by cofix discriminated else end exists exists2 fix for"
+    keywords="${keywords} forall fun if in lazymatch let match multimatch return then using where with"
+    keywords="${keywords} inside outside"
 
-        # These are (part of) coq top level commands
-        commands="Abort About Add Admitted All Arguments Axiom Back BackTo"
-        commands="${commands} Canonical Cd Check Coercion CoFixpoint Collection Compute Conjecture Context Contextual Corollary"
-        commands="${commands} Declare Defined Definition Delimit Drop End Eval Example Existential Export"
-        commands="${commands} Fact Fail File Fixpoint Focus From Function Generalizable Global Goal Grab"
-        commands="${commands} Hint Hypotheses Hypothesis Immediate Implicit Import Include Inductive"
-        commands="${commands} Lemma Let Library Load LoadPath Local Locate Module No Notation Opaque"
-        commands="${commands} Parameter Parameters Primitive Print Proof Property Proposition Pwd Qed Quit"
-        commands="${commands} Rec Record Redirect Register Remark Remove Require Reset"
-        commands="${commands} Section Search SearchAbout SearchHead SearchPattern SearchRewrite Show Strategy"
-        commands="${commands} Test Theorem Time Timeout Transparent Types Universes Undo Unfocus Unfocused Unset Variable Variables"
+    # These are (part of) coq top level commands
+    commands="Abort About Add Admitted All Arguments Axiom Back BackTo"
+    commands="${commands} Canonical Cd Check Coercion CoFixpoint Collection Compute Conjecture Context Contextual Corollary"
+    commands="${commands} Declare Defined Definition Delimit Drop End Eval Example Existential Export"
+    commands="${commands} Fact Fail File Fixpoint Focus From Function Generalizable Global Goal Grab"
+    commands="${commands} Hint Hypotheses Hypothesis Immediate Implicit Import Include Inductive"
+    commands="${commands} Lemma Let Library Load LoadPath Local Locate Module No Notation Opaque"
+    commands="${commands} Parameter Parameters Primitive Print Proof Property Proposition Pwd Qed Quit"
+    commands="${commands} Rec Record Redirect Register Remark Remove Require Reset"
+    commands="${commands} Section Search SearchAbout SearchHead SearchPattern SearchRewrite Show Strategy"
+    commands="${commands} Test Theorem Time Timeout Transparent Types Universes Undo Unfocus Unfocused Unset Variable Variables"
 
-        # These are (part of) coq's builtin tactics
-        tactics="abstract absurd admit all apply assert assert_fails"
-        tactics="${tactics} assert_succeeds assumption auto autoapply"
-        tactics="${tactics} autorewrite autounfold btauto by case cbn"
-        tactics="${tactics} cbv change clear clearbody cofix compare"
-        tactics="${tactics} compute congr congruence constructor contradict"
-        tactics="${tactics} cut cutrewrite cycle decide decompose dependent"
-        tactics="${tactics} destruct discriminate do done double"
-        tactics="${tactics} eapply eassert eauto eexact elim elimtype exact exfalso"
-        tactics="${tactics} fail field first firstorder fix fold functional"
-        tactics="${tactics} generalize guard have hnf idtac induction injection"
-        tactics="${tactics} instantiate intro intros intuition inversion"
-        tactics="${tactics} inversion_clear lapply lazy last move omega"
-        tactics="${tactics} pattern pose progress red refine reflexivity"
-        tactics="${tactics} remember rename repeat replace rewrite right ring"
-        tactics="${tactics} set setoid_reflexivity setoid_replace setoid_rewrite"
-        tactics="${tactics} setoid_symmetry setoid_transitivity simpl simple"
-        tactics="${tactics} simplify_eq solve specialize split start stop"
-        tactics="${tactics} subst symmetry tauto transitivity trivial try"
-        tactics="${tactics} under unfold unify unlock"
+    # These are (part of) coq's builtin tactics
+    tactics="abstract absurd admit all apply assert assert_fails"
+    tactics="${tactics} assert_succeeds assumption auto autoapply"
+    tactics="${tactics} autorewrite autounfold btauto by case cbn"
+    tactics="${tactics} cbv change clear clearbody cofix compare"
+    tactics="${tactics} compute congr congruence constructor contradict"
+    tactics="${tactics} cut cutrewrite cycle decide decompose dependent"
+    tactics="${tactics} destruct discriminate do done double"
+    tactics="${tactics} eapply eassert eauto eexact elim elimtype exact exfalso"
+    tactics="${tactics} fail field first firstorder fix fold functional"
+    tactics="${tactics} generalize guard have hnf idtac induction injection"
+    tactics="${tactics} instantiate intro intros intuition inversion"
+    tactics="${tactics} inversion_clear lapply lazy last move omega"
+    tactics="${tactics} pattern pose progress red refine reflexivity"
+    tactics="${tactics} remember rename repeat replace rewrite right ring"
+    tactics="${tactics} set setoid_reflexivity setoid_replace setoid_rewrite"
+    tactics="${tactics} setoid_symmetry setoid_transitivity simpl simple"
+    tactics="${tactics} simplify_eq solve specialize split start stop"
+    tactics="${tactics} subst symmetry tauto transitivity trivial try"
+    tactics="${tactics} under unfold unify unlock"
 
-        echo declare-option str-list coq_static_words ${keywords} ${commands} ${tactics}
+    echo declare-option str-list coq_static_words ${keywords} ${commands} ${tactics}
 
-        keywords_regex=$(echo ${keywords} | tr ' ' '|')
-        printf %s "
-            add-highlighter shared/coq/command/ regex \b(${keywords_regex})\b 0:keyword
-        "
-        commands_regex=$(echo ${commands} | tr ' ' '|')
-        printf %s "
-            add-highlighter shared/coq/command/ regex ^[\h\n]*(${commands_regex})\b 0:variable
-        "
+    keywords_regex=$(echo ${keywords} | tr ' ' '|')
+    printf %s "
+        add-highlighter shared/coq/command/ regex \b(${keywords_regex})\b 0:keyword
+    "
+    commands_regex=$(echo ${commands} | tr ' ' '|')
+    printf %s "
+        add-highlighter shared/coq/command/ regex ^[\h\n]*(${commands_regex})\b 0:variable
+    "
 
-        tactics_regex=$(echo ${tactics} | tr ' ' '|')
-        printf %s "
-            add-highlighter shared/coq/command/ regex \b(${tactics_regex})\b 0:keyword
-        "
-    }
+    tactics_regex=$(echo ${tactics} | tr ' ' '|')
+    printf %s "
+        add-highlighter shared/coq/command/ regex \b(${tactics_regex})\b 0:keyword
+    "
+}
 
 # Indentation
 # -----------
@@ -109,10 +109,10 @@ provide-module coq %{
 # not based on explicit, unique delimiters, like braces in C-family.
 # So it is difficult to properly indent using only regex...
 # Hence here only a simple mechanism of copying indent is done.
-    define-command -hidden coq-copy-indent-on-newline %{
-        evaluate-commands -draft -itersel %{
-            try %{ execute-keys -draft k <a-x> s ^\h+ <ret> y gh j P }
-        }
+define-command -hidden coq-copy-indent-on-newline %{
+    evaluate-commands -draft -itersel %{
+        try %{ execute-keys -draft k <a-x> s ^\h+ <ret> y gh j P }
+    }
 }
 
 }