fact: Definition ucomp1 {A B} (t: ttac A) (u: ttac B) : ttac A := '(m: v1, gls1) <- t; match gls1 with | [m: gl] => '(m: v2, gls) <- u; open_and_apply (exact v2) gl;; M.ret (m: v1, gls) | _ => mfail "more than a goal"%string end.
imports: Mtac2(Base Datatypes List Sorts tactics.Tactics) Strings.String Strings.String