Merge pull request #686 from L-TChen/agda-#5716

Make `cubical` compatible with `agda/agda#5716`
agda · Jan 14, 2022 · 8dea02e · 8dea02e
2 parents dba1d1f + fb72fe2
commit 8dea02e
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/Cubical/Reflection/Base.agda b/Cubical/Reflection/Base.agda
@@ -46,9 +46,9 @@ 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)
+extend*Context : ∀ {ℓ} {A : Type ℓ} → R.Telescope → R.TC A → R.TC A
+extend*Context []             tac = tac
+extend*Context ((s , a) ∷ as) tac = R.extendContext s a (extend*Context as tac)
 
 makeAuxiliaryDef : String → R.Type → R.Term → R.TC R.Term
 makeAuxiliaryDef s ty term =