aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-05-28 20:11:06 +0200
committerPierre-Marie Pédrot2018-05-28 20:11:06 +0200
commita205bb9f2a93396aad154ec50f6f122cbd46811c (patch)
treecd1ad9834fa9e6391193b377cc4533f9eba702c5 /kernel/typeops.ml
parent81535edc4b21015bd63d23e57ca9d707b4b71f6b (diff)
parent131ac2af3778a741f5f33e212ef4a57f7a91d20a (diff)
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
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 be4c0e1ecc..fd9cefb2cf 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -221,7 +221,7 @@ let check_cast env c ct k expected_type =
try
match k with
| VMcast ->
- vm_conv CUMUL env ct expected_type
+ Vconv.vm_conv CUMUL env ct expected_type
| DEFAULTcast ->
default_conv ~l2r:false CUMUL env ct expected_type
| REVERTcast ->