@@ -326,10 +326,14 @@ namespace Tactics
326326 ||| the body. Requires that the hole be in binding form (use
327327 ||| `attack`).
328328 |||
329− ||| @ n the name to use for the argument, or `Nothing` to use the name
330− ||| in the corresponding hole type (a dependent function)
331− intro : (n : Maybe TTName) -> Elab ()
332− intro n = prim__Intro n
329+ ||| @ n the name to use for the argument
330+ intro : (n : TTName) -> Elab ()
331+ intro n = prim__Intro (Just n)
332+
333+ ||| Introduce a lambda binding around the current hole and focus on
334+ ||| the body, using the name provided by the type of the hole.
335+ intro' : Elab ()
336+ intro' = prim__Intro Nothing
333337
334338 ||| Introduce a dependent function type binding into the current hole,
335339 ||| and focus on the body.