+ (*let res' =
+ List.map snd res in*)
+ let order_goal_list proof goal1 goal2 =
+ let _,metasenv,_,_ = proof in
+ let (ey1, ty1) =
+ let (_, ey ,ty) = CicUtil.lookup_meta goal1 metasenv in
+ (ey, ty) in
+ let (ey2, ty2) =
+ let (_, ey ,ty) = CicUtil.lookup_meta goal2 metasenv in
+ (ey, ty) in
+ let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
+ let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey1 ty2 in
+ let prop1 = if CicReduction.are_convertible
+ ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
+ else 1 in
+ let prop2 = if CicReduction.are_convertible
+ ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
+ else 1 in
+ prop1 - prop2 in
+ List.map (fun (level,(proof,goallist)) -> (proof, (List.stable_sort (order_goal_list proof) goallist))) res