diff options
| author | Maxime Dénès | 2019-04-14 14:02:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-15 15:28:09 +0200 |
| commit | 7205996bf25a542224c815b38f92da0ffef76b5d (patch) | |
| tree | 4853a361c9a1efe4f3d4163f47c0fa4cc514ce05 /kernel/nativecode.ml | |
| parent | 137e8b1636fa0b25c232ed42944ecaed058732ee (diff) | |
[native compiler] Remove unused universe argument in Lmakeblock
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|]) |