do not import specializations cache

Kha · Oct 5, 2022 · 456b4fa · 456b4fa
1 parent 95af593
commit 456b4fa
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Compiler/Specialize.lean b/src/Lean/Compiler/Specialize.lean
@@ -108,7 +108,7 @@ builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecSt
   registerSimplePersistentEnvExtension {
     name          := `specExt,
     addEntryFn    := SpecState.addEntry,
-    addImportedFn := fun es => (mkStateFromImportedEntries SpecState.addEntry {} es).switch
+    addImportedFn := fun es => (mkStateFromImportedEntries (fun | s, SpecEntry.cache .. => s | s, i => SpecState.addEntry s i) {} es).switch
   }
 
 @[export lean_add_specialization_info]