diff options
| author | filliatr | 1999-10-08 08:18:57 +0000 |
|---|---|---|
| committer | filliatr | 1999-10-08 08:18:57 +0000 |
| commit | fd28f10096f82ef133bbf10512c8bee617b6b8b3 (patch) | |
| tree | 96892fb5b66038cef8ca48b0cc3f0383e38fc9a5 /kernel/closure.ml | |
| parent | 610caabdaac2f9ca635737839f645cc870d83975 (diff) | |
deplacements des var. ex. hors du noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@93 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 49be8a1a5d..a7ee12c3e4 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -10,7 +10,6 @@ open Inductive open Environ open Instantiate open Univ -open Evd let stats = ref false @@ -136,7 +135,7 @@ let red_under (md,r) rk = type ('a, 'b) infos = { i_flags : flags; i_repr : ('a, 'b) infos -> constr -> 'a; - i_env : 'b unsafe_env; + i_env : unsafe_env; i_tab : (constr, 'a) Hashtbl.t } let const_value_cache info c = @@ -150,8 +149,8 @@ let const_value_cache info c = Some v | None -> None -let infos_under { i_flags = flg; i_repr = rfun; i_env = sigma; i_tab = tab } = - { i_flags = flags_under flg; i_repr = rfun; i_env = sigma; i_tab = tab } +let infos_under { i_flags = flg; i_repr = rfun; i_env = env; i_tab = tab } = + { i_flags = flags_under flg; i_repr = rfun; i_env = env; i_tab = tab } (**** Call by value reduction ****) @@ -465,10 +464,10 @@ and cbv_norm_value info = function (* reduction under binders *) type 'a cbv_infos = (cbv_value, 'a) infos (* constant bodies are normalized at the first expansion *) -let create_cbv_infos flgs sigma = +let create_cbv_infos flgs env = { i_flags = flgs; i_repr = (fun old_info c -> cbv_stack_term old_info TOP ESID c); - i_env = sigma; + i_env = env; i_tab = Hashtbl.create 17 } |