Merge pull request #3024 from ahmadsalim/fix/matchapply
Fixed matchApply to use `Prim__MatchApply`
commit3c839ae678e6afb63ed7b994f5d009277cae6b23
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 8 Mar 2016, 09:49 (11 years ago)
parentf173060923ef5f
libs/prelude/Language/Reflection/Elab.idr+1−1
@@ -335,7 +335,7 @@ namespace Tactics
335335
336336 export
337337 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
339339
340340 ||| Move the focus to the specified hole. Fails if the hole does not
341341 ||| exist.