diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c879cab9df..375f3184de 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1274,7 +1274,7 @@ let ml_of_instance instance u = | Lint tag -> MLapp(MLprimitive Mk_int, [|MLint tag|]) - | Lmakeblock (prefix,(cn,_u),_,args) -> + | Lmakeblock (prefix,cn,_,args) -> let args = Array.map (ml_of_lam env l) args in MLconstruct(prefix,cn,args) | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) |