+ let rec metas_of_term_and_types t =
+ let metas = CicUtil.metas_of_term t in
+ let types =
+ List.flatten
+ (List.map
+ (fun (i,_) -> try
+ let _,_,ty = CicUtil.lookup_meta i body_metasenv in metas_of_term_and_types ty
+ with CicUtil.Meta_not_found _ -> [])
+ metas)
+ in
+ metas @ types
+ in
+ let sorted_metas_of_term world t =
+ let metas = metas_of_term_and_types t in
+ (* this check should be useless *)
+ let metas = List.filter (fun (i,_)->List.exists (fun (j,_,_) -> j=i) world) metas in
+ let order_metas metasenv metas =
+ let module OT = struct type t = int let compare = Pervasives.compare end in
+ let module S = HTopoSort.Make (OT) in
+ let dep i =
+ try
+ let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in
+ let metas = List.map fst (CicUtil.metas_of_term ty) in
+ HExtlib.list_uniq (List.sort Pervasives.compare metas)
+ with Not_found -> []
+ in
+ S.topological_sort (List.map (fun (i,_) -> i) metas) dep
+ in
+ order_metas world metas
+ in