@@ -8,8 +8,7 @@ import Prelude.Maybe
8import Prelude.Monad
8import Prelude.Monad
9import Language.Reflection
9import Language.Reflection
11−%access private
11+abstract
13data Tactical : Type -> Type where
12data Tactical : Type -> Type where
14 -- obligatory control stuff
13 -- obligatory control stuff
15 prim__PureTactical : a -> Tactical a
14 prim__PureTactical : a -> Tactical a
@@ -67,6 +66,7 @@ getGoal = prim__Goal
68getHoles : Tactical (List TTName)
67getHoles : Tactical (List TTName)
69getHoles = prim__Holes
68getHoles = prim__Holes
70getGuess : Tactical (Maybe TT)
70getGuess : Tactical (Maybe TT)
71getGuess = prim__Guess
71getGuess = prim__Guess