spacemacs-coq-layer.patch

diff --git layers/+lang/coq/README.org layers/+lang/coq/README.org
index 526751d..9944aa3 100644
--- layers/+lang/coq/README.org
+++ layers/+lang/coq/README.org
@@ -14,6 +14,8 @@
    - [[#prover-queries][Prover queries]]
    - [[#moving-the-point][Moving the point]]
    - [[#inserting][Inserting]]
+ - [[#faq][FAQ]]
+   - [[#there-are-empty-square-boxes-in-place-of-math-operators][There are empty square boxes in place of math operators]]
 
 * Description
 This layer adds support for the [[https://coq.inria.fr/][Coq]] proof assistant (adapted from
@@ -35,6 +37,8 @@ Linux users can build from source or consult with their own package managers.
 proof assistants.
 
 To install, run the following commands:
+*Note*: The =make= step is recommended but optional. Compilation has been known
+to fail on Windows, but Proof General should work regardless.
 
 #+BEGIN_SRC sh
 git clone https://github.com/ProofGeneral/PG ~/.emacs.d/private/PG
@@ -101,4 +105,19 @@ The mnemonic for =a= is "ask".
 | ~M-S-RET~   | Insert =match goal with= branch                                 |
 
 Note the last two are regular =company-coq= bindings, left alone since they are
-most useful in insert mode.
+most useful in insert mode. The full =company-coq= tutorial showcasing all
+available =company-coq= keybindings can be accessed at any time using =SPC SPC
+company-coq-tutorial=.
+
+* FAQ
+** There are empty square boxes in place of math operators
+Math symbols present in your buffer (e.g. forall exists) will attempt to be
+prettified, if you are seeing empty square boxes this means an appropriate math
+symbol cannot be found in your font. You can either install a appropriate math
+font, or disable the feature by adding the following snippet to the your
+=dotspacemacs/user-config=.
+
+#+BEGIN_SRC emacs-lisp
+(with-eval-after-load 'company-coq
+  (add-to-list 'company-coq-disabled-features 'prettify-symbols))
+#+END_SRC
diff --git layers/+lang/coq/packages.el layers/+lang/coq/packages.el
index 4f5c6fe..039cac0 100644
--- layers/+lang/coq/packages.el
+++ layers/+lang/coq/packages.el
@@ -13,8 +13,8 @@
 
 (setq coq-packages
       '(
-        (proof-general :location local)
         (company-coq :toggle (configuration-layer/package-usedp 'company))
+        (proof-general :location local)
         smartparens
         vi-tilde-fringe
         ))
@@ -40,17 +40,17 @@
     :load-path "~/.emacs.d/private/PG/generic"
     :config
     (progn
-      (spacemacs|diminish outline-minor-mode)
+      (spacemacs|diminish company-coq-mode)
       (spacemacs|diminish holes-mode)
       (spacemacs|diminish hs-minor-mode)
+      (spacemacs|diminish outline-minor-mode)
+      (spacemacs|diminish proof-active-buffer-fake-minor-mode)
+      (spacemacs|diminish yas-minor-mode " ⓨ" " y")
 
-      (setq proof-splash-seen t)
-
-      (setq proof-three-window-mode-policy 'hybrid)
-
-      ;; I don't know who wants to evaluate comments
-      ;; one-by-one, but I don't.
-      (setq proof-script-fly-past-comments t)
+      (setq company-coq-disabled-features '(hello)
+            proof-three-window-mode-policy 'hybrid
+            proof-script-fly-past-comments t
+            proof-splash-seen t)
 
       (dolist (prefix '(("ml" . "pg/layout")
                         ("mp" . "pg/prover")
@@ -93,8 +93,7 @@
         "ga" 'proof-goto-command-start
         "ge" 'proof-goto-command-end
         ;; Insertions
-        "ie" 'coq-end-Section)
-      )))
+        "ie" 'coq-end-Section))))
 
 (defun coq/post-init-smartparens ()
   (spacemacs/add-to-hooks