diff options
Diffstat (limited to 'kernel/conv_oracle.ml')
| -rw-r--r-- | kernel/conv_oracle.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 3b01538b92..3f1cf92487 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -71,7 +71,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = | _ -> Cpred.add c oracle.cst_trstate in { oracle with cst_opacity; cst_trstate; } - | RelKey _ -> Errors.error "set_strategy: RelKey" + | RelKey _ -> CErrors.error "set_strategy: RelKey" let fold_strategy f { var_opacity; cst_opacity; } accu = let fvar id lvl accu = f (VarKey id) lvl accu in @@ -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) |