diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 9bc67b5ad..dc98cc65d 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -247,8 +247,8 @@ let info_env info = info.i_cache.i_env let rec assoc_defined id = function | [] -> raise Not_found -| (_, None, _) :: ctxt -> assoc_defined id ctxt -| (id', Some c, _) :: ctxt -> +| Context.Named.Declaration.LocalAssum _ :: ctxt -> assoc_defined id ctxt +| Context.Named.Declaration.LocalDef (id', c, _) :: ctxt -> if Id.equal id id' then c else assoc_defined id ctxt let ref_value_cache ({i_cache = cache} as infos) ref = @@ -285,9 +285,9 @@ let defined_rels flags env = let ctx = rel_context env in let len = List.length ctx in let ans = Array.make len None in - let iter i (_, b, _) = match b with - | None -> () - | Some _ -> Array.unsafe_set ans i b + let iter i = function + | Context.Rel.Declaration.LocalAssum _ -> () + | Context.Rel.Declaration.LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b) in let () = List.iteri iter ctx in ans |