chore: compatibility with latest nightlies + releases (#41)

leanprover · Sep 3, 2024 · 4f4ac30 · 4f4ac30
1 parent f611fda
commit 4f4ac30
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -20,9 +20,11 @@ jobs:
           - "4.8.0"
           - "4.9.0"
           - "4.10.0"
-          - "4.11.0-rc3"
+          - "4.11.0"
+          - "4.12.0-rc1"
           - "nightly-2024-08-09"
           - "nightly-2024-08-29"
+          - "nightly-2024-09-03"
         platform:
           - os: ubuntu-latest
             installer: |

diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean
@@ -76,6 +76,7 @@ def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32
 
 def mkRefIdentFVar [Monad m] [MonadEnv m] (id : FVarId) : m Lean.Lsp.RefIdent := do
   pure %first_succeeding [
+    .fvar (← getEnv).mainModule.toString id.name.toString,
     .fvar (← getEnv).mainModule id,
     .fvar id
   ]
@@ -84,6 +85,9 @@ def refIdentCase (ri : Lsp.RefIdent)
     (onFVar : FVarId → α)
     (onConst : Name → α) : α :=
   %first_succeeding [
+    match ri with
+    | .fvar _ id => onFVar ⟨id.toName⟩
+    | .const _ x => onConst x.toName,
     match ri with
     | .fvar _ id => onFVar id
     | .const _ x => onConst x,