@@ -255,10 +255,8 @@ namespace Tactics
255255 ||| Attempt to apply an operator to fill the current hole,
256256 ||| potentially solving arguments by unification.
257257 |||
258− ||| The return value is a list of pairs of names, one for each input
259− ||| argument. The first projection of these pairs is the original
260− ||| name of the argument, from the type declaration, and the second
261− ||| projection is the hole into which it is placed.
258+ ||| The return value is the list of holes established for the
259+ ||| arguments to the function.
262260 |||
263261 ||| Note that not all of the returned hole names still exist, as
264262 ||| they may have been solved.
@@ -267,18 +265,15 @@ namespace Tactics
267265 |||
268266 ||| @ argSpec instructions for finding the arguments to the term,
269267 ||| where the Boolean states whether or not to attempt to solve
270− ||| the argument and the Int gives the priority in which to do
271− ||| so
268+ ||| the argument by unification.
272269 apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
273270 apply tm argSpec = map snd <$> prim__Apply tm argSpec
274271
275272 ||| Attempt to apply an operator to fill the current hole,
276− ||| potentially solving arugments by matching.
273+ ||| potentially solving arguments by matching.
277274 |||
278− ||| The return value is a list of pairs of names, one for each input
279− ||| argument. The first projection of these pairs is the original
280− ||| name of the argument, from the type declaration, and the second
281− ||| projection is the hole into which it is placed.
275+ ||| The return value is the list of holes established for the
276+ ||| arguments to the function.
282277 |||
283278 ||| Note that not all of the returned hole names still exist, as
284279 ||| they may have been solved.
@@ -287,8 +282,8 @@ namespace Tactics
287282 |||
288283 ||| @ argSpec instructions for finding the arguments to the term,
289284 ||| where the Boolean states whether or not to attempt to solve
290− ||| the argument and the Int gives the priority in which to do
291− ||| so
285+ ||| the argument by matching.
286+
292287 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
293288 matchApply tm argSpec = map snd <$> prim__Apply tm argSpec
294289