+ let flatten_fast subst =
+ let resolve_meta (i, (context, term, ty)) subst =
+ let term = CicMetaSubst.apply_subst subst term in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ (i, (context, term, ty))
+ in
+ let resolve_meta t s = profiler3.HExtlib.profile (resolve_meta t) s in
+ let filter j (i,_) = i <> j in
+ let filter a b = profiler4.HExtlib.profile (filter a) b in
+ List.fold_left
+ (fun subst (j,(c,t,ty)) as s ->
+ let s = resolve_meta s subst in
+ s::(List.filter (filter j) subst))
+ subst subst
+ in
+ (*let flatten subst = profiler.HExtlib.profile flatten subst in*)
+ let flatten_fast subst = profiler2.HExtlib.profile flatten_fast subst in
+ (*let subst = flatten subst in*)
+(* let subst = flatten_fast subst in*)