fact: Definition move_until_aux {A} (x: A) : gtactic (mlist name) := (fix move_until_aux (accu: mlist name) (hyps: mlist Hyp) := \tactic g=> match hyps with | [m: ] => M.raise NotAVar | (ahyp y _ :m: hyps) => mif M.cumul UniMatchNoRed x y then ret accu g else name <- M.pretty_print y; cmove_back y (move_until_aux (TheName name :m: accu) hyps) g end) [m:] =<< M.hyps.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic Sorts MTeleMatch) Strings.String NArith.BinNat NArith.BinNatDef