@@ -1066,7 +1066,7 @@ elab ist info emode opts fn tm
10661066 delayElab $ do focus h
10671067 dotterm
10681068 elab' ina fc t
1069− elab' ina _ (PRunTactics fc tm) =
1069+ elab' ina fc (PRunTactics fc' tm) =
10701070 do attack
10711071 n <- getNameFrom (sMN 0 "tacticScript")
10721072 n' <- getNameFrom (sMN 0 "tacticExpr")
@@ -1075,10 +1075,10 @@ elab ist info emode opts fn tm
10751075 movelast n
10761076 letbind n' scriptTy (Var n)
10771077 focus n
1078− elab' ina (Just fc) tm
1078+ elab' ina (Just fc') tm
10791079 env <- get_env
10801080 ctxt <- get_context
1081− runTactical fc ctxt env (P Bound n' Erased)
1081+ runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)
10821082 solve
10831083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
10841084