fact: Definition with_goal_sort (F : forall {s : Sort} (T : s), ttac T) (e : Exception) : tactic := fun g => match g with | Metavar s T g => '(m: t, gs) <- F T; o <- M.inst_evar g t; match o with | mSome _ => gs <- M.map (fun x => M.ret (mpair tt x)) gs; M.ret gs | mNone => raise e end end.
imports: Mtac2(Base Datatypes List Sorts tactics.Tactics) Strings.String Strings.String