+module OT =
+ struct
+ type t = int * NCic.conjecture
+ let compare (i,_) (j,_) = Pervasives.compare i j
+ end
+
+module MS = HTopoSort.Make(OT)
+let relations_of_menv subst m c =
+ let i, (_, ctx, ty) = c in
+ let m = List.filter (fun (j,_) -> j <> i) m in
+ let m_ty = metas_of_term subst ctx ty in
+ let m_ctx =
+ snd
+ (List.fold_right
+ (fun i (ctx,res) ->
+ (i::ctx),
+ (match i with
+ | _,NCic.Decl ty -> metas_of_term subst ctx ty
+ | _,NCic.Def (t,ty) ->
+ metas_of_term subst ctx ty @ metas_of_term subst ctx t) @ res)
+ ctx ([],[]))
+ in
+ let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in
+ List.filter (fun (i,_) -> List.exists ((=) i) metas) m
+;;
+
+let sort_metasenv subst (m : NCic.metasenv) =
+ (MS.topological_sort m (relations_of_menv subst m) : NCic.metasenv)
+;;