@@ -1066,7 +1066,7 @@ elab ist info emode opts fn tm
1066 delayElab $ do focus h
1066 delayElab $ do focus h
1068 elab' ina fc t
1068 elab' ina fc t
1069− elab' ina _ (PRunTactics fc tm) =
1069+ elab' ina fc (PRunTactics fc' tm) =
1070 do attack
1070 do attack
1071 n <- getNameFrom (sMN 0 "tacticScript")
1071 n <- getNameFrom (sMN 0 "tacticScript")
1072 n' <- getNameFrom (sMN 0 "tacticExpr")
1072 n' <- getNameFrom (sMN 0 "tacticExpr")
@@ -1075,10 +1075,10 @@ elab ist info emode opts fn tm
1075 movelast n
1075 movelast n
1076 letbind n' scriptTy (Var n)
1076 letbind n' scriptTy (Var n)
1078− elab' ina (Just fc) tm
1078+ elab' ina (Just fc') tm
1079 env <- get_env
1079 env <- get_env
1080 ctxt <- get_context
1080 ctxt <- get_context
1081− runTactical fc ctxt env (P Bound n' Erased)
1081+ runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)
1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x