fact: Definition test_Prop := ( match_goal with | [[?P : Prop |- P]] => mmatch P return M (P *m _) with | True =n> TT.idtac : M _ | _ => mfail "[P] not forwarded as exactly [P] to [match_goal] branch" end end)%MC%TT.
imports: Mtac2(Mtac2 Ttactics) Coq(String)