+
+
+ (* menv sorting *)
+module OT =
+ struct
+ type t = Cic.conjecture
+ let compare (i,_,_) (j,_,_) = Pervasives.compare i j
+ end
+module MS = HTopoSort.Make(OT)
+let relations_of_menv m c =
+ let i, ctx, ty = c in
+ let m = List.filter (fun (j,_,_) -> j <> i) m in
+ let m_ty = List.map fst (CicUtil.metas_of_term ty) in
+ let m_ctx =
+ List.flatten
+ (List.map
+ (function
+ | None -> []
+ | Some (_,Cic.Decl t)
+ | Some (_,Cic.Def (t,None)) ->
+ List.map fst (CicUtil.metas_of_term ty)
+ | Some (_,Cic.Def (t,Some ty)) ->
+ List.map fst (CicUtil.metas_of_term ty) @
+ List.map fst (CicUtil.metas_of_term t))
+ 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 (m : Cic.metasenv) =
+ (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
+;;
+