fact: Definition mmatch'' {A:Type} {P: A -> Type} (E : Exception) (y : A) (failure : gtactic (P y)) (ps : mlist (Tbranch A P)) : gtactic (P y) := fun g => M.mmatch'' E y (failure g) (mmap (branch_map y g) ps).
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic intf.Sorts) Strings.String NArith.BinNat NArith.BinNatDef