diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr
index 1c3a1cec3df..58c3dafabef 100644
--- a/src/Core/Binary.idr
+++ b/src/Core/Binary.idr
@@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 20230414 * 100 + 0
+ttcVersion = 2023_08_01_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index 499bac7dd85..0e2f5a6fd9d 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -370,7 +370,7 @@ mutual
   desugarB side ps (PUnquote fc tm)
       = pure $ IUnquote fc !(desugarB side ps tm)
   desugarB side ps (PRunElab fc tm)
-      = pure $ IRunElab fc !(desugarB side ps tm)
+      = pure $ IRunElab fc True !(desugarB side ps tm)
   desugarB side ps (PHole fc br holename)
       = do when br $ update Syn { bracketholes $= ((UN (Basic holename)) ::) }
            pure $ IHole fc holename
diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr
index 33a72cabcd6..de3cfe51a80 100644
--- a/src/Idris/Resugar.idr
+++ b/src/Idris/Resugar.idr
@@ -387,7 +387,7 @@ mutual
       = do ds' <- traverse toPDecl ds
            pure $ PQuoteDecl fc (catMaybes ds')
   toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm))
-  toPTerm p (IRunElab fc tm) = pure (PRunElab fc !(toPTerm argPrec tm))
+  toPTerm p (IRunElab fc _ tm) = pure (PRunElab fc !(toPTerm argPrec tm))
 
   toPTerm p (IUnifyLog fc _ tm) = toPTerm p tm
   toPTerm p (Implicit fc True) = pure (PImplicit fc)
diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr
index 3e45e772cd7..09567214c7c 100644
--- a/src/TTImp/Elab/Ambiguity.idr
+++ b/src/TTImp/Elab/Ambiguity.idr
@@ -145,7 +145,7 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
         = if (Context.Macro `elem` flags def) && notLHS mode
              then alternativeFirstSuccess $ reverse $
                     allSplits args <&> \(macroArgs, extArgs) =>
-                      (IRunElab fc $ ICoerced fc $ IVar fc n `buildAlt` macroArgs) `buildAlt` extArgs
+                      (IRunElab fc False $ ICoerced fc $ IVar fc n `buildAlt` macroArgs) `buildAlt` extArgs
              else wrapDot prim est mode n (map (snd . snd) args)
                     (definition def) (buildAlt (IVar fc n) args)
       where
diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr
index f3edfbd4fdb..05515a3d568 100644
--- a/src/TTImp/Elab/RunElab.idr
+++ b/src/TTImp/Elab/RunElab.idr
@@ -245,12 +245,12 @@ checkRunElab : {vars : _} ->
                {auto o : Ref ROpts REPLOpts} ->
                RigCount -> ElabInfo ->
                NestedNames vars -> Env Term vars ->
-               FC -> RawImp -> Maybe (Glued vars) ->
+               FC -> (requireExtension : Bool) -> RawImp -> Maybe (Glued vars) ->
                Core (Term vars, Glued vars)
-checkRunElab rig elabinfo nest env fc script exp
+checkRunElab rig elabinfo nest env fc reqExt script exp
     = do expected <- mkExpected exp
          defs <- get Ctxt
-         unless (isExtension ElabReflection defs) $
+         unless (not reqExt || isExtension ElabReflection defs) $
              throw (GenericMsg fc "%language ElabReflection not enabled")
          let n = NS reflectionNS (UN $ Basic "Elab")
          elabtt <- appCon fc defs n [expected]
diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr
index ae1128f414f..29946f31944 100644
--- a/src/TTImp/Elab/Term.idr
+++ b/src/TTImp/Elab/Term.idr
@@ -204,8 +204,8 @@ checkTerm rig elabinfo nest env (IQuoteDecl fc ds) exp
     = checkQuoteDecl rig elabinfo nest env fc ds exp
 checkTerm rig elabinfo nest env (IUnquote fc tm) exp
     = throw (GenericMsg fc "Can't escape outside a quoted term")
-checkTerm rig elabinfo nest env (IRunElab fc tm) exp
-    = checkRunElab rig elabinfo nest env fc tm exp
+checkTerm rig elabinfo nest env (IRunElab fc re tm) exp
+    = checkRunElab rig elabinfo nest env fc re tm exp
 checkTerm {vars} rig elabinfo nest env (IPrimVal fc c) exp
     = do let (cval, cty) = checkPrim {vars} fc c
          checkExp rig elabinfo env fc cval (gnf env cty) exp
diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr
index 68e3a0891ed..0f9a0184cdb 100644
--- a/src/TTImp/Reflect.idr
+++ b/src/TTImp/Reflect.idr
@@ -605,7 +605,7 @@ mutual
         = pure (Ref tfc Bound t)
     reflect fc defs lhs env (IUnquote tfc t)
         = throw (InternalError "Can't reflect an unquote: escapes should be lifted out")
-    reflect fc defs lhs env (IRunElab tfc t)
+    reflect fc defs lhs env (IRunElab tfc _ t)
         = throw (InternalError "Can't reflect a %runElab")
     reflect fc defs lhs env (IPrimVal tfc t)
         = do fc' <- reflect fc defs lhs env tfc
diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
index 0c1bd6e1256..c28f47d4e9e 100644
--- a/src/TTImp/TTImp.idr
+++ b/src/TTImp/TTImp.idr
@@ -112,7 +112,7 @@ mutual
        IQuoteName : FC -> Name -> RawImp' nm
        IQuoteDecl : FC -> List (ImpDecl' nm) -> RawImp' nm
        IUnquote : FC -> RawImp' nm -> RawImp' nm
-       IRunElab : FC -> RawImp' nm -> RawImp' nm
+       IRunElab : FC -> (requireExtension : Bool) -> RawImp' nm -> RawImp' nm
 
        IPrimVal : FC -> (c : Constant) -> RawImp' nm
        IType : FC -> RawImp' nm
@@ -200,7 +200,7 @@ mutual
       show (IQuoteName fc tm) = "(%quotename " ++ show tm ++ ")"
       show (IQuoteDecl fc tm) = "(%quotedecl " ++ show tm ++ ")"
       show (IUnquote fc tm) = "(%unquote " ++ show tm ++ ")"
-      show (IRunElab fc tm) = "(%runelab " ++ show tm ++ ")"
+      show (IRunElab fc _ tm) = "(%runelab " ++ show tm ++ ")"
       show (IPrimVal fc c) = show c
       show (IHole _ x) = "?" ++ x
       show (IUnifyLog _ lvl x) = "(%logging " ++ show lvl ++ " " ++ show x ++ ")"
@@ -601,7 +601,7 @@ findIBinds (IDelay fc tm) = findIBinds tm
 findIBinds (IForce fc tm) = findIBinds tm
 findIBinds (IQuote fc tm) = findIBinds tm
 findIBinds (IUnquote fc tm) = findIBinds tm
-findIBinds (IRunElab fc tm) = findIBinds tm
+findIBinds (IRunElab fc _ tm) = findIBinds tm
 findIBinds (IBindHere _ _ tm) = findIBinds tm
 findIBinds (IBindVar _ n) = [n]
 findIBinds (IUpdate fc updates tm)
@@ -637,7 +637,7 @@ findImplicits (IDelay fc tm) = findImplicits tm
 findImplicits (IForce fc tm) = findImplicits tm
 findImplicits (IQuote fc tm) = findImplicits tm
 findImplicits (IUnquote fc tm) = findImplicits tm
-findImplicits (IRunElab fc tm) = findImplicits tm
+findImplicits (IRunElab fc _ tm) = findImplicits tm
 findImplicits (IBindVar _ n) = [n]
 findImplicits (IUpdate fc updates tm)
     = findImplicits tm ++ concatMap (findImplicits . getFieldUpdateTerm) updates
@@ -870,7 +870,7 @@ getFC (IQuote x _) = x
 getFC (IQuoteName x _) = x
 getFC (IQuoteDecl x _) = x
 getFC (IUnquote x _) = x
-getFC (IRunElab x _) = x
+getFC (IRunElab x _ _) = x
 getFC (IAs x _ _ _ _) = x
 getFC (Implicit x _) = x
 getFC (IWithUnambigNames x _ _) = x
diff --git a/src/TTImp/TTImp/Functor.idr b/src/TTImp/TTImp/Functor.idr
index ecd33bcad37..d4d42a4dd22 100644
--- a/src/TTImp/TTImp/Functor.idr
+++ b/src/TTImp/TTImp/Functor.idr
@@ -62,8 +62,8 @@ mutual
       = IQuoteDecl fc (map (map f) ds)
     map f (IUnquote fc t)
       = IUnquote fc (map f t)
-    map f (IRunElab fc t)
-      = IRunElab fc (map f t)
+    map f (IRunElab fc re t)
+      = IRunElab fc re (map f t)
     map f (IPrimVal fc c)
       = IPrimVal fc c
     map f (IType fc)
diff --git a/src/TTImp/TTImp/TTC.idr b/src/TTImp/TTImp/TTC.idr
index 7a705245594..9255a888916 100644
--- a/src/TTImp/TTImp/TTC.idr
+++ b/src/TTImp/TTImp/TTC.idr
@@ -72,8 +72,8 @@ mutual
         = do tag 23; toBuf b fc; toBuf b t
     toBuf b (IUnquote fc t)
         = do tag 24; toBuf b fc; toBuf b t
-    toBuf b (IRunElab fc t)
-        = do tag 25; toBuf b fc; toBuf b t
+    toBuf b (IRunElab fc re t)
+        = do tag 25; toBuf b fc; toBuf b re; toBuf b t
 
     toBuf b (IPrimVal fc y)
         = do tag 26; toBuf b fc; toBuf b y
@@ -164,8 +164,8 @@ mutual
                         pure (IQuoteDecl fc y)
                24 => do fc <- fromBuf b; y <- fromBuf b
                         pure (IUnquote fc y)
-               25 => do fc <- fromBuf b; y <- fromBuf b
-                        pure (IRunElab fc y)
+               25 => do fc <- fromBuf b; re <- fromBuf b; y <- fromBuf b
+                        pure (IRunElab fc re y)
 
                26 => do fc <- fromBuf b; y <- fromBuf b
                         pure (IPrimVal fc y)
diff --git a/src/TTImp/TTImp/Traversals.idr b/src/TTImp/TTImp/Traversals.idr
index b44e4db9948..0cefdbdfa66 100644
--- a/src/TTImp/TTImp/Traversals.idr
+++ b/src/TTImp/TTImp/Traversals.idr
@@ -119,7 +119,7 @@ parameters (f : RawImp' nm -> RawImp' nm)
   mapTTImp (IQuoteName fc n) = f $ IQuoteName fc n
   mapTTImp (IQuoteDecl fc xs) = f $ IQuoteDecl fc (assert_total $ map mapImpDecl xs)
   mapTTImp (IUnquote fc t) = f $ IUnquote fc (mapTTImp t)
-  mapTTImp (IRunElab fc t) = f $ IRunElab fc (mapTTImp t)
+  mapTTImp (IRunElab fc re t) = f $ IRunElab fc re (mapTTImp t)
   mapTTImp (IPrimVal fc c) = f $ IPrimVal fc c
   mapTTImp (IType fc) = f $ IType fc
   mapTTImp (IHole fc str) = f $ IHole fc str
diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr
index 5dc4e0f7260..6af1ee5a8f5 100644
--- a/src/TTImp/Utils.idr
+++ b/src/TTImp/Utils.idr
@@ -187,7 +187,7 @@ findBindableNamesQuot env used (IUnifyLog fc k x)
 findBindableNamesQuot env used (IQuote fc x) = []
 findBindableNamesQuot env used (IQuoteName fc x) = []
 findBindableNamesQuot env used (IQuoteDecl fc xs) = []
-findBindableNamesQuot env used (IRunElab fc x) = []
+findBindableNamesQuot env used (IRunElab fc _ x) = []
 
 export
 findUniqueBindableNames :
diff --git a/tests/Main.idr b/tests/Main.idr
index d0338662cb4..02d8a408f8d 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -250,7 +250,8 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing
        "reflection005", "reflection006", "reflection007", "reflection008",
        "reflection009", "reflection010", "reflection011", "reflection012",
        "reflection013", "reflection014", "reflection015", "reflection016",
-       "reflection017", "reflection018", "reflection019", "reflection020"]
+       "reflection017", "reflection018", "reflection019", "reflection020",
+       "reflection021"]
 
 idrisTestsWith : TestPool
 idrisTestsWith = MkTestPool "With abstraction" [] Nothing
diff --git a/tests/idris2/reflection021/DeclMacro.idr b/tests/idris2/reflection021/DeclMacro.idr
new file mode 100644
index 00000000000..dec9f5251d6
--- /dev/null
+++ b/tests/idris2/reflection021/DeclMacro.idr
@@ -0,0 +1,10 @@
+module DeclMacro
+
+import public Language.Reflection
+
+export %macro
+macroFun : Nat -> Elab Nat
+macroFun x = pure $ x + 1
+
+justScript : Nat -> Elab Nat
+justScript x = pure $ x + 2
diff --git a/tests/idris2/reflection021/UseMacroWithoutExtension.idr b/tests/idris2/reflection021/UseMacroWithoutExtension.idr
new file mode 100644
index 00000000000..53807aba5c3
--- /dev/null
+++ b/tests/idris2/reflection021/UseMacroWithoutExtension.idr
@@ -0,0 +1,14 @@
+module UseMacroWithoutExtension
+
+import DeclMacro
+
+useMacro : Nat
+useMacro = macroFun 5
+
+useMacroCorr : UseMacroWithoutExtension.useMacro = 6
+useMacroCorr = Refl
+
+failing "%language ElabReflection not enabled"
+
+  stillCan'tUseRunElabWithoutExtension : Nat
+  stillCan'tUseRunElabWithoutExtension = %runElab justScript 4
diff --git a/tests/idris2/reflection021/expected b/tests/idris2/reflection021/expected
new file mode 100644
index 00000000000..4f5eed7b642
--- /dev/null
+++ b/tests/idris2/reflection021/expected
@@ -0,0 +1,2 @@
+1/2: Building DeclMacro (DeclMacro.idr)
+2/2: Building UseMacroWithoutExtension (UseMacroWithoutExtension.idr)
diff --git a/tests/idris2/reflection021/run b/tests/idris2/reflection021/run
new file mode 100644
index 00000000000..63a90724a41
--- /dev/null
+++ b/tests/idris2/reflection021/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check UseMacroWithoutExtension.idr
diff --git a/tests/idris2/reflection021/test.ipkg b/tests/idris2/reflection021/test.ipkg
new file mode 100644
index 00000000000..2c5b5ab52de
--- /dev/null
+++ b/tests/idris2/reflection021/test.ipkg
@@ -0,0 +1 @@
+package a-test