fact: Definition progress {A} (t : gtactic A) : gtactic A := fun '(Metavar _ _ g) => r <- t (Metavar _ _ g); match r with | [m:(m: x,g')] => mmatch AnyMetavar _ _ g with | g' => M.raise NoProgress | _ => M.ret [m:(m: x,g')] end | _ => M.ret r end.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic Sorts MTeleMatch) Strings.String NArith.BinNat NArith.BinNatDef