@@ -24,11 +24,11 @@ import Language.Reflection.Utils
24intros : Elab ()
24intros : Elab ()
25intros = do g <- getGoal
25intros = do g <- getGoal
26 case snd g of
26 case snd g of
27− `(~_ -> ~_) => intro Nothing
27+ `(~_ -> ~_) => intro'
28 _ => return ()
28 _ => return ()
30foo : Nat -> Nat
30foo : Nat -> Nat
31−foo = %runElab (do intro (Just (UN "fnord"))
31+foo = %runElab (do intro (UN "fnord")
32 fill `(plus ~(Var (UN "fnord")) ~(Var (UN "fnord")))
32 fill `(plus ~(Var (UN "fnord")) ~(Var (UN "fnord")))