@@ -627,8 +627,11 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
627 x@(Bind y (Pi _ s _) _) -> x
627 x@(Bind y (Pi _ s _) _) -> x
628 _ -> hnf ctxt env t
628 _ -> hnf ctxt env t
629 case t' of
629 case t' of
630− Bind y (Pi _ s _) t -> -- trace ("in type " ++ show t') $
630+ Bind y (Pi _ s _) t ->
631+ -- It's important that this be subst and not updsubst,
632+ -- because we want to substitute even in portions of
633+ -- terms that we know do not contain holes.
631− let t' = updsubst y (P Bound n s) t in
634+ let t' = subst y (P Bound n s) t in
632 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
635 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
633 _ -> lift $ tfail $ CantIntroduce t'
636 _ -> lift $ tfail $ CantIntroduce t'
634intro n ctxt env _ = fail "Can't introduce here."
637intro n ctxt env _ = fail "Can't introduce here."