From c2da7afd76b8294bbb4ca7582a7d8f243571889e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 11 Dec 2021 14:26:32 +0100
Subject: [PATCH] chore: Update compiler and fix minor breaking change

---
 DocGen4/Process.lean | 2 +-
 lean-toolchain       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 6116f9b..89b7313 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -96,7 +96,7 @@ def prettyPrintTerm (expr : Expr) : MetaM Syntax := do
 def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
   let env ← getEnv
   let type ← prettyPrintTerm v.type
-  let doc := findDocString? env v.name
+  let doc ← findDocString? env v.name
   match ←findDeclarationRanges? v.name with
   -- TODO: Maybe selection range is more relevant? Figure this out in the future
   | some range => return Info.mk ⟨v.name, type⟩ doc range.range
diff --git a/lean-toolchain b/lean-toolchain
index 22206e9..45db7af 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2021-11-26
+leanprover/lean4:nightly-2021-12-10