@@ -173,30 +173,30 @@ elaborating_app = do ES (ps, _) _ _ <- get
173173
174174-- Some handy gadgets for pulling out bits of state
175175
176−-- get the global context
176+-- | Get the global context
177177get_context :: Elab' aux Context
178178get_context = do ES p _ _ <- get
179179 return $! (context (fst p))
180180
181−-- update the context
181+-- | Update the context.
182182-- (should only be used for adding temporary definitions or all sorts of
183183-- stuff could go wrong)
184184set_context :: Context -> Elab' aux ()
185185set_context ctxt = do ES (p, a) logs prev <- get
186186 put (ES (p { context = ctxt }, a) logs prev)
187187
188−-- get the proof term
188+-- | get the proof term
189189get_term :: Elab' aux Term
190190get_term = do ES p _ _ <- get
191191 return $! (getProofTerm (pterm (fst p)))
192192
193−-- get the proof term
193+-- | get the proof term
194194update_term :: (Term -> Term) -> Elab' aux ()
195195update_term f = do ES (p,a) logs prev <- get
196196 let p' = p { pterm = mkProofTerm (f (getProofTerm (pterm p))) }
197197 put (ES (p', a) logs prev)
198198
199−-- get the local context at the currently in focus hole
199+-- | get the local context at the currently in focus hole
200200get_env :: Elab' aux Env
201201get_env = do ES p _ _ <- get
202202 lift $ envAtFocus (fst p)
@@ -213,14 +213,14 @@ get_probs :: Elab' aux Fails
213213get_probs = do ES p _ _ <- get
214214 return $! (problems (fst p))
215215
216−-- Return recently solved names (that is, the names solved since the
216+-- | Return recently solved names (that is, the names solved since the
217217-- last call to get_recents)
218218get_recents :: Elab' aux [Name]
219219get_recents = do ES (p, a) l prev <- get
220220 put (ES (p { recents = [] }, a) l prev)
221221 return (recents p)
222222
223−-- get the current goal type
223+-- | get the current goal type
224224goal :: Elab' aux Type
225225goal = do ES p _ _ <- get
226226 b <- lift $ goalAtFocus (fst p)
@@ -233,7 +233,7 @@ is_guess = do ES p _ _ <- get
233233 Guess _ _ -> return True
234234 _ -> return False
235235
236−-- Get the guess at the current hole, if there is one
236+-- | Get the guess at the current hole, if there is one
237237get_guess :: Elab' aux Type
238238get_guess = do ES p _ _ <- get
239239 b <- lift $ goalAtFocus (fst p)
@@ -241,7 +241,7 @@ get_guess = do ES p _ _ <- get
241241 Guess t v -> return $! v
242242 _ -> fail "Not a guess"
243243
244−-- typecheck locally
244+-- | Typecheck locally
245245get_type :: Raw -> Elab' aux Type
246246get_type tm = do ctxt <- get_context
247247 env <- get_env
@@ -254,7 +254,7 @@ get_type_val tm = do ctxt <- get_context
254254 (val, ty) <- lift $ check ctxt env tm
255255 return $! (finalise val, finalise ty)
256256
257−-- get holes we've deferred for later definition
257+-- | get holes we've deferred for later definition
258258get_deferred :: Elab' aux [Name]
259259get_deferred = do ES p _ _ <- get
260260 return $! (deferred (fst p))
@@ -271,17 +271,18 @@ checkInjective (tm, l, r) = do ctxt <- get_context
271271 isInj ctxt (Bind _ (Pi _ _ _) sc) = True
272272 isInj ctxt _ = False
273273
274−-- get instance argument names
274+-- | get instance argument names
275275get_instances :: Elab' aux [Name]
276276get_instances = do ES p _ _ <- get
277277 return $! (instances (fst p))
278278
279−-- get auto argument names
279+-- | get auto argument names
280280get_autos :: Elab' aux [(Name, [Name])]
281281get_autos = do ES p _ _ <- get
282282 return $! (autos (fst p))
283283
284−-- given a desired hole name, return a unique hole name
284+-- | given a desired hole name, return a unique hole name
285+unique_hole :: Name -> Elab' aux Name
285286unique_hole = unique_hole' False
286287
287288unique_hole' :: Bool -> Name -> Elab' aux Name