[ re agda#703, agda#743 ] Remove extend*Context

L-TChen · Mar 27, 2022 · 423ee6c · 423ee6c
1 parent 909fc4f
commit 423ee6c
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/Cubical/Reflection/Base.agda b/Cubical/Reflection/Base.agda
@@ -46,10 +46,6 @@ hlam str t = R.lam R.hidden (R.abs str t)
 
 newMeta = R.checkType R.unknown
 
-extend*Context : ∀ {ℓ} {A : Type ℓ} → List (R.Arg R.Type) → R.TC A → R.TC A
-extend*Context [] tac = tac
-extend*Context (a ∷ as) tac = R.extendContext a (extend*Context as tac)
-
 makeAuxiliaryDef : String → R.Type → R.Term → R.TC R.Term
 makeAuxiliaryDef s ty term =
   R.freshName s >>= λ name →