From 9a6bf855882bc6c8c3674476bd3cfbc270f4242a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 19 Apr 2022 20:18:28 +0200 Subject: [PATCH] chore: update toolchain --- DocGen4/Process.lean | 3 ++- lean-toolchain | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 4fd0c85..d815f96 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -142,7 +142,8 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do options := ← getOptions currNamespace := ← getCurrNamespace openDecls := ← getOpenDecls - fileMap := default + fileMap := default, + ngen := ← getNGen } pure $ tagExprInfos ctx infos tt diff --git a/lean-toolchain b/lean-toolchain index 4b053c2..4d9c593 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-04-04 +leanprover/lean4:nightly-2022-04-16