diff options
Diffstat (limited to 'pretyping/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index bd427ecd0..ac4e3b306 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -378,8 +378,8 @@ and nf_predicate env ind mip params v pT = | _, _ -> false, nf_type env v let native_norm env sigma c ty = - if !Flags.no_native_compiler then - error "Native_compute reduction has been disabled" + if Coq_config.no_native_compiler then + error "Native_compute reduction has been disabled at configure time." else let penv = Environ.pre_env env in (* |