fixes

leanprover · Nov 4, 2024 · 3fcc4b2 · 3fcc4b2
1 parent f9cdc62
commit 3fcc4b2
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/DocGen4/Output/References.lean b/DocGen4/Output/References.lean
@@ -74,7 +74,7 @@ def refItem (ref : BibItem) (backrefs : Array BackrefItem) : BaseHtmlM Html := d
     if backrefs.isEmpty then
       pure (.raw "")
     else
-      pure <small>[(← backrefs.mapIdxM toHtml).foldl (· ++ ·) #[]]</small>)
+      pure <small>[(← backrefs.mapFinIdxM toHtml).foldl (· ++ ·) #[]]</small>)
   pure <|
     <li id={s!"ref_{ref.citekey}"}>
       <a href={s!"#ref_{ref.citekey}"}>{.text ref.tag}</a>

diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean
@@ -34,7 +34,7 @@ def getFieldTypes (v : InductiveVal) : MetaM (Array NameInfo) := do
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
-  let parents := getParentStructures env v.name
+  let parents ← getAllParentStructures v.name
   let ctorVal := getStructureCtor env v.name
   let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type
   match getStructureInfo? env v.name with

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "107e98b3e7603628d9bfd817b4704488d8a25e96",
+   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",