When the tactic faces with this goal:
KTraceMatch (KTP_NegClass (KAP_KRecv MP_M :: nil))
(KRecv c (BadTag tag) :: nil)
It applies KTM_NegClass, and results in the following goal :
forall kap : KActionPat,
In kap (KAP_KRecv MP_M :: nil) ->
~ KActionMatch kap (KRecv c (BadTag tag))
But ktm_basic doesn't deal with this shape of goal.
When the tactic faces with this goal:
KTraceMatch (KTP_NegClass (KAP_KRecv MP_M :: nil))
(KRecv c (BadTag tag) :: nil)
It applies KTM_NegClass, and results in the following goal :
forall kap : KActionPat,
In kap (KAP_KRecv MP_M :: nil) ->
~ KActionMatch kap (KRecv c (BadTag tag))
But ktm_basic doesn't deal with this shape of goal.