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