@@ -8,8 +8,7 @@ import Prelude.Maybe
88import Prelude.Monad
99import Language.Reflection
1010
11−%access private
12−
11+abstract
1312data Tactical : Type -> Type where
1413 -- obligatory control stuff
1514 prim__PureTactical : a -> Tactical a
@@ -67,6 +66,7 @@ getGoal = prim__Goal
6766
6867getHoles : Tactical (List TTName)
6968getHoles = prim__Holes
69+
7070getGuess : Tactical (Maybe TT)
7171getGuess = prim__Guess
7272