diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index cfc286135d..30a346c910 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -20,7 +20,6 @@ open Util open Names open Term open Vars -open Univ open Environ open Closure open Esubst @@ -177,7 +176,7 @@ let convert_instances ~flex u u' (s, check) = let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else match k1, k2 with - | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' -> + | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' -> if Univ.Instance.equal u u' then cuniv else let flex = evaluable_constant cst (info_env infos) @@ -682,7 +681,7 @@ let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> - Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); + Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); gen_conv cv_pb env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = |