+ (*let res' =
+ List.map snd res in*)
+ let order_goal_list proof goal1 goal2 =
+ let _,metasenv,_,_ = proof in
+ let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
+ let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
+(*
+ prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
+*)
+ let ty_sort1,u = (*TASSI: FIXME *)
+ CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph in
+(*
+ prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
+*)
+ let ty_sort2,u1 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 u in
+(*
+ prerr_endline "DOPO LA SECONDA TYPE OF " ;
+*)
+ let b,u2 =
+ CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 u1 in
+ let prop1 = if b then 0 else 1 in
+ let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 u2 in
+ let prop2 = if b then 0 else 1 in
+ prop1 - prop2 in
+ List.map (
+ fun (level,(proof,goallist)) ->
+ (proof, (List.stable_sort (order_goal_list proof) goallist))
+ ) res