summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs')
-rw-r--r--src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs b/src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs
index cc05e25..81765fc 100644
--- a/src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs
+++ b/src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs
@@ -155,8 +155,8 @@ instantiateTel s tel = liftTCM $ do
mkSubst :: [Maybe Term] -> S.Substitution
mkSubst s = rho 0 s'
where s' = s
- rho i (Nothing : s) = var i :# rho (i + 1) s
- rho i (Just u : s) = u :# rho i s
+ rho i (Nothing : s) = consS (var i) $ rho (i + 1) s
+ rho i (Just u : s) = consS u $ rho i s
rho i [] = raiseS i
-- | Produce a nice error message when splitting failed