Imported Upstream version 8.5~beta3+dfsg

1 files changed, 10 insertions, 5 deletions

diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 3b01538b..ec2c334b 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -82,12 +82,17 @@ let fold_strategy f { var_opacity; cst_opacity; } accu =
 let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate)
 
 (* Unfold the first constant only if it is "more transparent" than the
-   second one. In case of tie, expand the second one. *)
+   second one. In case of tie, use the recommended default. *)
 let oracle_order f o l2r k1 k2 =
   match get_strategy o f k1, get_strategy o f k2 with
-    | Expand, _ -> true
-    | Level n1, Opaque -> true
-    | Level n1, Level n2 -> n1 < n2
-    | _ -> l2r (* use recommended default *)
+  | Expand, Expand -> l2r
+  | Expand, (Opaque | Level _) -> true
+  | (Opaque | Level _), Expand -> false
+  | Opaque, Opaque -> l2r
+  | Level _, Opaque -> true
+  | Opaque, Level _ -> false
+  | Level n1, Level n2 ->
+     if Int.equal n1 n2 then l2r
+     else n1 < n2
 
 let get_strategy o = get_strategy o (fun x -> x)