From 030dd3d7778f3a7980a926ad40c3cdd37747a863 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Wed, 22 May 2024 07:21:24 +0100
Subject: [PATCH] chore: remove unused change_mlir_context (#325)

This meta-code breaks with the next lean update. As it is unused, we
drop it beforehand.
---
 SSA/Core/Tactic.lean | 29 -----------------------------
 1 file changed, 29 deletions(-)

diff --git a/SSA/Core/Tactic.lean b/SSA/Core/Tactic.lean
index 90523a89b..2bf52f99a 100644
--- a/SSA/Core/Tactic.lean
+++ b/SSA/Core/Tactic.lean
@@ -12,35 +12,6 @@ namespace SSA
 
 open Ctxt (Var Valuation DerivedCtxt)
 
-section
-
-open Lean Meta Elab.Tactic Qq
-
-/-- Given a `V : Valuation Γ`, fully reduce the context `Γ` in the type of `V` -/
-elab "change_mlir_context " V:ident : tactic => do
-  let V : Name := V.getId
-  withMainContext do
-    let ctx ← getLCtx
-    let Vdecl : LocalDecl ← match ctx.findFromUserName? V with
-      | some decl => pure decl
-      | none => throwError f!"Failed to find variable `{V}` in the local context"
-
-    -- Assert that the type of `V` is `Ctxt.Valuation ?Γ`
-    let Ty ← mkFreshExprMVarQ q(Type)
-    let Γ  ← mkFreshExprMVarQ q(Ctxt $Ty)
-    let G  ← mkFreshExprMVarQ q(TyDenote $Ty)
-    let _  ← assertDefEqQ Vdecl.type q(@Ctxt.Valuation $Ty $G $Γ)
-
-    -- Reduce the context `Γ`
-    let Γr ← ctxtNf Γ
-    let Γr : Q(Ctxt $Ty) := Γr
-
-    let goal ← getMainGoal
-    let newGoal ← goal.changeLocalDecl Vdecl.fvarId q(Valuation $Γr)
-    replaceMainGoal [newGoal]
-
-end
-
 open Lean Elab Tactic Meta
 
 /--