aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/typeops.ml')
-rw-r--r--kernel/typeops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 8895bae5d..70f6fd803 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -310,7 +310,7 @@ let judge_of_cast env cj k tj =
| NATIVEcast ->
let sigma = Nativelambda.empty_evars in
mkCast (cj.uj_val, k, expected_type),
- native_conv CUMUL sigma env cj.uj_type expected_type
+ Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type
in
{ uj_val = c;
uj_type = expected_type }