- 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
+ 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