mtac2: merge [Mgoal_patt] with [Mpatt] so the notations can be shared.
mtac2: notations for goal matching and goal patterns