aboutsummaryrefslogtreecommitdiff
path: root/kernel/fast_typeops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/fast_typeops.ml')
-rw-r--r--kernel/fast_typeops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index d22abff10c..063c9cf126 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -227,7 +227,7 @@ let judge_of_cast env c ct k expected_type =
default_conv ~l2r:true CUMUL env ct expected_type
| NATIVEcast ->
let sigma = Nativelambda.empty_evars in
- native_conv CUMUL sigma env ct expected_type
+ Nativeconv.native_conv CUMUL sigma env ct expected_type
with NotConvertible ->
error_actual_type env (make_judge c ct) expected_type