@@ -91,7 +91,7 @@ newHole hint ty =
9191|||
9292||| @ tm the term that has the right type for the hole
9393exact : (tm : Raw) -> Elab ()
94−exact tm = do apply tm []
94+exact tm = do fill tm
9595 solve
9696
9797||| Introduce as many names as possible, returning them.
@@ -178,7 +178,7 @@ data Infer : Type where
178178total
179179inferType : (tac : Elab ()) -> Elab (TT, TT)
180180inferType tac =
181− case fst !(runElab `(Infer) (startInfer *> tac)) of
181+ case fst !(runElab `(Infer) (do startInfer; tac)) of
182182 `(MkInfer ~ty ~tm) => return (tm, ty)
183183 _ => fail [TextPart "Not infer"]
184184 where