From 79a108a8568dc35791351bdabec5217008fb01e1 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Wed, 10 Nov 2021 17:52:45 +0100
Subject: [PATCH 1/2] Suggested fix for indentation problem

---
 docs/editor.md | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/docs/editor.md b/docs/editor.md
index 438252da9..bce31d0d2 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -125,6 +125,27 @@ results in a decent choice for the symbols used in Iris:
 (set-fontset-font t nil (font-spec :name "Symbola"))
 ```
 
+### Automated Indentation
+
+The default indentation configuration of company-coq is not compatible with the Iris syntax.
+As a result, automatic indentation will indent lines incorrectly.
+
+To solve some of these indentation errors you can add the following line to your Emacs
+initialisation file:
+```
+(setq coq-smie-user-tokens
+	'(("∗" . "*")
+	  ("-∗" . "->")
+	  ("∗-∗" . "<->")
+	  ("==∗" . "->")
+	  ("⊢" . "->")
+	  ("⊣⊢" . "<->")
+	  ("⋅" . "*")
+	  (":>" . ":=")))
+```
+This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the
+closely related Coq symbols (e.g. `->`).
+
 ## CoqIDE 8.9 and earlier on Linux (ibus-m17n)
 
 On Linux with old versions of CoqIDE you can use the Intelligent
-- 
GitLab


From d1131ebd8f765823e6ec4cbec4de10191b0903db Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Wed, 10 Nov 2021 18:31:17 +0100
Subject: [PATCH 2/2] Added support for `by` and `forall`

---
 docs/editor.md | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/docs/editor.md b/docs/editor.md
index bce31d0d2..d59d4a550 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -134,14 +134,16 @@ To solve some of these indentation errors you can add the following line to your
 initialisation file:
 ```
 (setq coq-smie-user-tokens
-	'(("∗" . "*")
-	  ("-∗" . "->")
-	  ("∗-∗" . "<->")
-	  ("==∗" . "->")
-	  ("⊢" . "->")
-	  ("⊣⊢" . "<->")
-	  ("⋅" . "*")
-	  (":>" . ":=")))
+    '(("∗" . "*")
+      ("-∗" . "->")
+      ("∗-∗" . "<->")
+      ("==∗" . "->")
+      ("⊢" . "->")
+      ("⊣⊢" . "<->")
+      ("⋅" . "*")
+      (":>" . ":=")
+      ("by" . "now")
+      ("forall" . "now")))
 ```
 This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the
 closely related Coq symbols (e.g. `->`).
-- 
GitLab