@@ -1542,7 +1542,7 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1542 (Var (reflm "TT"))
1542 (Var (reflm "TT"))
1543 | n == tacN "prim__SourceLocation", [] <- args
1543 | n == tacN "prim__SourceLocation", [] <- args
1544 = fmap fst . get_type_val $
1544 = fmap fst . get_type_val $
1545− reflectFC fc
1545+ reflectFC fc
1546 | n == tacN "prim__Env", [] <- args
1546 | n == tacN "prim__Env", [] <- args
1547 = do env <- get_env
1547 = do env <- get_env
1548 fmap fst . get_type_val $ reflectEnv env
1548 fmap fst . get_type_val $ reflectEnv env
@@ -1550,7 +1550,7 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1550 = do parts <- reifyReportParts (eval errs)
1550 = do parts <- reifyReportParts (eval errs)
1551 lift . tfail $ ReflectionError [parts] (Msg "")
1551 lift . tfail $ ReflectionError [parts] (Msg "")
1552 | n == tacN "prim__PureTactical", [_a, tm] <- args
1552 | n == tacN "prim__PureTactical", [_a, tm] <- args
1553− = return tm
1553+ = return tm
1554 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1554 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1555 = do let first' = eval first
1555 = do let first' = eval first
1556 res <- runTacTm first'
1556 res <- runTacTm first'