diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index bf39fa42b..bad28487c 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -197,7 +197,6 @@ let unfold_red kn = * is stored in the table. * * i_rels is the array of free rel variables together with their optional * body - * * i_vars is the list of _defined_ named variables. * * ref_value_cache searchs in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't @@ -230,11 +229,16 @@ type 'a infos = { i_env : env; i_sigma : existential -> constr option; i_rels : constr option array; - i_vars : (Id.t * constr) list; i_tab : 'a KeyTable.t } let info_flags info = info.i_flags +let rec assoc_defined id = function +| [] -> raise Not_found +| (_, None, _) :: ctxt -> assoc_defined id ctxt +| (id', Some c, _) :: ctxt -> + if Id.equal id id' then c else assoc_defined id ctxt + let ref_value_cache info ref = try Some (KeyTable.find info.i_tab ref) @@ -250,7 +254,7 @@ let ref_value_cache info ref = | None -> raise Not_found | Some t -> lift n t end - | VarKey id -> Id.List.assoc id info.i_vars + | VarKey id -> assoc_defined id (named_context info.i_env) | ConstKey cst -> constant_value info.i_env cst in let v = info.i_repr info body in @@ -264,16 +268,6 @@ let ref_value_cache info ref = let evar_value info ev = info.i_sigma ev -let defined_vars flags env = -(* if red_local_const (snd flags) then*) - Context.fold_named_context - (fun (id,b,_) e -> - match b with - | None -> e - | Some body -> (id, body)::e) - (named_context env) ~init:[] -(* else []*) - let defined_rels flags env = (* if red_local_const (snd flags) then*) let ctx = rel_context env in @@ -293,7 +287,6 @@ let create mk_cl flgs env evars = i_env = env; i_sigma = evars; i_rels = defined_rels flgs env; - i_vars = defined_vars flgs env; i_tab = KeyTable.create 17 } |