diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2762a52a16..834c27969e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -606,7 +606,7 @@ let pb_equal = function let sort_cmp = sort_cmp -let test_conversion (f:?evars:'a->'b) env sigma x y = +let test_conversion (f: ?l2r:bool-> ?evars:'a->'b) env sigma x y = try let _ = f ~evars:(safe_evar_value sigma) env x y in true with NotConvertible -> false @@ -616,7 +616,7 @@ let is_conv env sigma = test_conversion Reduction.conv env sigma let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq -let test_trans_conversion (f:?evars:'a->'b) reds env sigma x y = +let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = try let _ = f ~evars:(safe_evar_value sigma) reds env x y in true with NotConvertible -> false | Anomaly _ -> error "Conversion test raised an anomaly" diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 31bf431da1..4610c06ce5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -325,7 +325,7 @@ let oracle_order env cf1 cf2 = | Some k1 -> match cf2 with | None -> Some true - | Some k2 -> Some (Conv_oracle.oracle_order k1 k2) + | Some k2 -> Some (Conv_oracle.oracle_order false k1 k2) let do_reduce ts (env, nb) sigma c = let (t, stack') = whd_betaiota_deltazeta_for_iota_state ts env sigma (c, empty_stack) in |