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