@@ -620,19 +620,19 @@ introTy ty n ctxt env _ = fail "Can't introduce here."
621intro :: Maybe Name -> RunTactic
621intro :: Maybe Name -> RunTactic
622intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
622intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
623− do let n = case mn of
626− let t' = case t of
623+ do let t' = case t of
627 x@(Bind y (Pi _ s _) _) -> x
624 x@(Bind y (Pi _ s _) _) -> x
628 _ -> hnf ctxt env t
625 _ -> hnf ctxt env t
629 case t' of
626 case t' of
630 Bind y (Pi _ s _) t ->
627 Bind y (Pi _ s _) t ->
631 -- It's important that this be subst and not updsubst,
631 -- It's important that this be subst and not updsubst,
632 -- because we want to substitute even in portions of
632 -- because we want to substitute even in portions of
633 -- terms that we know do not contain holes.
633 -- terms that we know do not contain holes.
634− let t' = subst y (P Bound n s) t in
634+ t' = subst y (P Bound n s) t
635− return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
635+ in return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
636 _ -> lift $ tfail $ CantIntroduce t'
636 _ -> lift $ tfail $ CantIntroduce t'
637intro n ctxt env _ = fail "Can't introduce here."
637intro n ctxt env _ = fail "Can't introduce here."