mtac2: add another test case for gmatch
mtac2: forgot to remove a part of the hack in the previous commit.
mtac2: [Run.run] now returns a [Proofview.tactic]
mtac2: extend [Proofview] so we can add goals to the current proofview