@@ -1311,17 +1311,21 @@ elab ist info emode opts fn tm
1311 do unless (ElabReflection `elem` idris_language_extensions ist) $
1311 do unless (ElabReflection `elem` idris_language_extensions ist) $
1312 lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")
1312 lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")
1314+ let elabName = sNS (sUN "Elab") ["Elab", "Reflection", "Language"]
1314 n <- getNameFrom (sMN 0 "tacticScript")
1315 n <- getNameFrom (sMN 0 "tacticScript")
1315− let scriptTy = RApp (Var (sNS (sUN "Elab")
1316+ let scriptTy = RApp (Var elabName) (Var unitTy)
1316− ["Elab", "Reflection", "Language"]))
1318 claim n scriptTy
1317 claim n scriptTy
1320 attack -- to get an extra hole
1320 attack -- to get an extra hole
1321 elab' ina (Just fc') tm
1321 elab' ina (Just fc') tm
1322 script <- get_guess
1322 script <- get_guess
1323 fullyElaborated script
1323 fullyElaborated script
1324 solve -- eliminate the hole. Because there are no references, the script is only in the binding
1324 solve -- eliminate the hole. Because there are no references, the script is only in the binding
1325+ ctxt <- get_context
1327+ (scriptTm, scriptTy) <- lift $ check ctxt [] (forget script)
1328+ lift $ converts ctxt env elabUnit scriptTy
1325 env <- get_env
1329 env <- get_env
1326 runElabAction info ist (maybe fc' id fc) env script ns
1330 runElabAction info ist (maybe fc' id fc) env script ns