From 4552729b88058946055dddde1533057e25bfc5a9 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 16 May 2018 00:06:51 +0200 Subject: Unify pre_env and env We now have only two notions of environments in the kernel: env and safe_env. --- pretyping/nativenorm.ml | 3 +-- pretyping/typing.ml | 5 +---- pretyping/vnorm.ml | 2 +- 3 files changed, 3 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 85911394f..978ceed1e 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -457,13 +457,12 @@ let native_norm env sigma c ty = if not Coq_config.native_compiler then user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else - let penv = Environ.pre_env env in (* Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1); Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2); *) let ml_filename, prefix = Nativelib.get_ml_filename () in - let code, upd = mk_norm_code penv (evars_of_evar_map sigma) prefix c in + let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in let profile = get_profiling_enabled () in match Nativelib.compile ml_filename code ~profile:profile with | true, fn -> diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 6bd75c93d..68f9610d1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -215,10 +215,7 @@ let judge_of_cast env sigma cj k tj = uj_type = expected_type } let enrich_env env sigma = - let penv = Environ.pre_env env in - let penv' = Pre_env.({ penv with env_stratification = - { penv.env_stratification with env_universes = Evd.universes sigma } }) in - Environ.env_of_pre_env penv' + set_universes env @@ Evd.universes sigma let check_fix env sigma pfix = let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 049c3aff5..a1ba4a6a9 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -383,7 +383,7 @@ let cbv_vm env sigma c t = (** This evar-normalizes terms beforehand *) let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in - let v = Vconv.val_of_constr env c in + let v = Csymtable.val_of_constr env c in EConstr.of_constr (nf_val env sigma v t) let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = -- cgit v1.2.3