diff options
Diffstat (limited to 'kernel/nativeconv.ml')
-rw-r--r-- | kernel/nativeconv.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index f51b58322..c07025660 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -136,9 +136,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu = aux 0 cu let native_conv_gen pb sigma env univs t1 t2 = - let penv = Environ.pre_env env in let ml_filename, prefix = get_ml_filename () in - let code, upds = mk_conv_code penv sigma prefix t1 t2 in + let code, upds = mk_conv_code env sigma prefix t1 t2 in match compile ml_filename code ~profile:false with | (true, fn) -> begin |