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 d517d215ed..9ce388929c 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -2130,7 +2130,7 @@ let compile_deps env sigma prefix init t = in aux env 0 init t -let compile_constant_field env _prefix con acc cb = +let compile_constant_field env con acc cb = let gl = compile_constant env empty_evars con cb in gl@acc |