diff --git a/src/Lean/Meta/Constructions/CtorElim.lean b/src/Lean/Meta/Constructions/CtorElim.lean
index 6efdd0a755..69943209fd 100644
--- a/src/Lean/Meta/Constructions/CtorElim.lean
+++ b/src/Lean/Meta/Constructions/CtorElim.lean
@@ -223,9 +223,11 @@ public def mkCtorElim (indName : Name) : MetaM Unit := do
   let recInfo ← getConstInfo (mkRecName indName)
   unless recInfo.levelParams.length > indVal.levelParams.length do return
 
-  mkCtorElimType indName
-  mkIndCtorElim indName
-  mkConstructorElim indName
+  -- Expose if indName is not private
+  withExporting (isExporting := ! isPrivateName indName) do
+    mkCtorElimType indName
+    mkIndCtorElim indName
+    mkConstructorElim indName
 
 
 /--
diff --git a/src/Lean/Meta/Constructions/CtorIdx.lean b/src/Lean/Meta/Constructions/CtorIdx.lean
index 6720879be4..f00b0e0746 100644
--- a/src/Lean/Meta/Constructions/CtorIdx.lean
+++ b/src/Lean/Meta/Constructions/CtorIdx.lean
@@ -33,7 +33,8 @@ returns the constructor index of the given value.
 Does nothing if `T` does not eliminate into `Type` or if `T` is unsafe.
 Assumes `T.casesOn` to be defined already.
 -/
-public def mkCtorIdx (indName : Name) : MetaM Unit := do
+public def mkCtorIdx (indName : Name) : MetaM Unit :=
+  withExporting (isExporting := ! isPrivateName indName) do
   prependError m!"failed to construct `T.ctorIdx` for `{.ofConstName indName}`:" do
     unless genCtorIdx.get (← getOptions) do return
     let declName := mkCtorIdxName indName
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..d8fc746d3a 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/issue10299.lean b/tests/lean/run/issue10299.lean
new file mode 100644
index 0000000000..05fe025a04
--- /dev/null
+++ b/tests/lean/run/issue10299.lean
@@ -0,0 +1,7 @@
+module
+
+/-! Tests that ctorIdx and constructor elims are exposed, i.e. reduce properly -/
+
+example : Nat.ctorIdx 0 = 0 := rfl
+
+example : Nat.succ.elim 1 rfl (fun n => n) = 0 := rfl