git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3024 from ahmadsalim/fix/matchapply
3c839aeDavid Christiansen
libs/prelude/Language/Reflection/Elab.idr+1−1
compare with master
unifiedsplit
@@ -335,7 +335,7 @@ namespace Tactics
335
335
336 export
336 export
337 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
337 matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
338− matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec
338+ matchApply tm argSpec = map snd <$> Prim__MatchApply tm argSpec
339
339
340 ||| Move the focus to the specified hole. Fails if the hole does not
340 ||| Move the focus to the specified hole. Fails if the hole does not
341 ||| exist.
341 ||| exist.