diff --git a/library/init/env_ext.lean b/library/init/env_ext.lean
index 7f9a576014..c5d227e461 100644
--- a/library/init/env_ext.lean
+++ b/library/init/env_ext.lean
@@ -11,9 +11,6 @@ Environment extensions:
 - protected
   * NameSet mProtected;
 
-- noncomputable
-  * NameSet
-
 - exportDecl: it is used to implement the `export` command
   * NameMap<List<exportDecl>> mNsMap;   // mapping from namespace to "export Declaration"
 
@@ -34,22 +31,6 @@ Environment extensions:
 - user attributes:
   * NameMap<attributePtr> mAttrs;
 
-- Bytecode
-  * unsignedMap<vmDecl>           mDecls;
-  * unsignedMap<vmCasesFunction> mCases;
-  * Name                            mMonitor;
-
-- Module
-  *  std::vector<moduleName> mDirectImports;
-  *  List<std::sharedPtr<modification const>> mModifications;
-  *  names        mModuleUnivs;
-  *  names        mModuleDecls;
-  *  NameSet     mModuleDefs;
-  *  NameSet     mImported;
-  *  // Map from Declaration Name to olean file where it was defined
-  *  NameMap<std::String>     mDecl2Olean;
-  *  NameMap<posInfo>        mDecl2PosInfo;
-
 - scopedExt: a general purpose scoped extension. It is used to implement
   * Parser/scanner tables
   * attributeManager (do we need them? we can try to keep user attributes only)