From 5a99cb326c9e9052e135cc63ed02b63371cff6d3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 18 Nov 2024 17:14:34 +1100
Subject: [PATCH] chore: make Lean.Elab.Command.mkMetaContext public (#6113)

---
 src/Lean/Elab/Command.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index d10fb3da6a..fa2f3fef00 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -555,7 +555,11 @@ private def getVarDecls (s : State) : Array Syntax :=
 instance {α} : Inhabited (CommandElabM α) where
   default := throw default
 
-private def mkMetaContext : Meta.Context := {
+/--
+The environment linter framework needs to be able to run linters with the same context
+as `liftTermElabM`, so we expose that context as a public function here.
+-/
+def mkMetaContext : Meta.Context := {
   config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }
 }