diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean
index 939edd9640..23fa7326ec 100644
--- a/Lake/Config/Load.lean
+++ b/Lake/Config/Load.lean
@@ -132,5 +132,5 @@ Load the package located in
 the given directory with the given configuration file.
 -/
 @[implementedBy loadUnsafe]
-constant load (dir : FilePath) (args : List String := [])
+opaque load (dir : FilePath) (args : List String := [])
 (configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogT IO Package
diff --git a/Lake/Config/Opaque.lean b/Lake/Config/Opaque.lean
index 849270a8ae..64ea8a483d 100644
--- a/Lake/Config/Opaque.lean
+++ b/Lake/Config/Opaque.lean
@@ -5,14 +5,14 @@ Authors: Mac Malone
 -/
 namespace Lake
 
-constant OpaquePackagePointed : NonemptyType.{0}
+opaque OpaquePackagePointed : NonemptyType.{0}
 
 /-- Opaque reference to a `Package` used for forward declaration. -/
 def OpaquePackage : Type := OpaquePackagePointed.type
 
 instance : Nonempty OpaquePackage := OpaquePackagePointed.property
 
-constant OpaqueWorkspacePointed : NonemptyType.{0}
+opaque OpaqueWorkspacePointed : NonemptyType.{0}
 
 /-- Opaque reference to a `Workspace` used for forward declaration. -/
 def OpaqueWorkspace : Type := OpaqueWorkspacePointed.type
diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean
index 076d539669..fb75f5661b 100644
--- a/Lake/Config/Package.lean
+++ b/Lake/Config/Package.lean
@@ -285,7 +285,7 @@ namespace OpaquePackage
 unsafe def unsafeMk (pkg : Package) : OpaquePackage :=
   unsafeCast pkg
 
-@[implementedBy unsafeMk] constant mk (pkg : Package) : OpaquePackage
+@[implementedBy unsafeMk] opaque mk (pkg : Package) : OpaquePackage
 
 instance : Coe Package OpaquePackage := ⟨mk⟩
 instance : Inhabited OpaquePackage := ⟨mk Inhabited.default⟩
@@ -293,7 +293,7 @@ instance : Inhabited OpaquePackage := ⟨mk Inhabited.default⟩
 unsafe def unsafeGet (self : OpaquePackage) : Package :=
   unsafeCast self
 
-@[implementedBy unsafeGet] constant get (self : OpaquePackage) : Package
+@[implementedBy unsafeGet] opaque get (self : OpaquePackage) : Package
 
 instance : Coe OpaquePackage Package := ⟨get⟩
 
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index b399cfd0cf..960c1016c8 100644
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@@ -30,7 +30,7 @@ namespace OpaqueWorkspace
 unsafe def unsafeMk (ws : Workspace) : OpaqueWorkspace :=
   unsafeCast ws
 
-@[implementedBy unsafeMk] constant mk (ws : Workspace) : OpaqueWorkspace
+@[implementedBy unsafeMk] opaque mk (ws : Workspace) : OpaqueWorkspace
 
 instance : Coe Workspace OpaqueWorkspace := ⟨mk⟩
 instance : Inhabited OpaqueWorkspace := ⟨mk Inhabited.default⟩
@@ -38,7 +38,7 @@ instance : Inhabited OpaqueWorkspace := ⟨mk Inhabited.default⟩
 unsafe def unsafeGet (self : OpaqueWorkspace) : Workspace :=
   unsafeCast self
 
-@[implementedBy unsafeGet] constant get (self : OpaqueWorkspace) : Workspace
+@[implementedBy unsafeGet] opaque get (self : OpaqueWorkspace) : Workspace
 
 instance : Coe OpaqueWorkspace Workspace := ⟨get⟩
 
diff --git a/Lake/DSL/Config.lean b/Lake/DSL/Config.lean
index 5faf74c9d0..0e1c16e165 100644
--- a/Lake/DSL/Config.lean
+++ b/Lake/DSL/Config.lean
@@ -13,13 +13,13 @@ open Lean Elab Term
 A dummy default constant for `__dir__` to make it type check
 outside Lakefile elaboration (e.g., when editing).
 -/
-constant dummyDir : System.FilePath
+opaque dummyDir : System.FilePath
 
 /--
 A dummy default constant for `__args__` to make it type check
 outside Lakefile elaboration (e.g., when editing).
 -/
-constant dummyArgs : List String
+opaque dummyArgs : List String
 
 /--
 A macro that expands to the path of package's directory
diff --git a/Lake/Util/EvalTerm.lean b/Lake/Util/EvalTerm.lean
index 6f5e9fbf74..ee3242fe0e 100644
--- a/Lake/Util/EvalTerm.lean
+++ b/Lake/Util/EvalTerm.lean
@@ -38,7 +38,7 @@ unsafe def unsafeEvalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α := do
     setEnv env
 
 @[implementedBy unsafeEvalTerm]
-constant evalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α
+opaque evalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α
 
 -- ## ToExpr Instances
 
diff --git a/examples/ffi/lib/lean/FFI.lean b/examples/ffi/lib/lean/FFI.lean
index 9ba99565ca..9652d99333 100644
--- a/examples/ffi/lib/lean/FFI.lean
+++ b/examples/ffi/lib/lean/FFI.lean
@@ -1,5 +1,5 @@
 @[extern "my_add"]
-constant myAdd : UInt32 → UInt32 → UInt32
+opaque myAdd : UInt32 → UInt32 → UInt32
 
 @[extern "my_lean_fun"]
-constant myLeanFun : IO PUnit
+opaque myLeanFun : IO PUnit