diff options
| author | Pierre-Marie Pédrot | 2014-02-07 16:46:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-02-11 13:14:58 +0100 |
| commit | 971f5d2ddff84a479022bb38af799f7e4166dea3 (patch) | |
| tree | deae1bd7cb1336e7775c08334a1df38a665a81a6 /pretyping | |
| parent | d8202af0887825d236c3e11704f266d8282c8aa7 (diff) | |
Made Pre_env.lazy_val opaque.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 24 |
1 files changed, 10 insertions, 14 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 264172d0c9..f4636cdaa4 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -493,20 +493,16 @@ let clear_hyps_in_evi evdref hyps concl ids = let c' = check_and_clear_in_constr evdref err ids c in if ob == ob' && c == c' then decl else (id, ob', c') in - let check_value vk = - match !vk with - | VKnone -> vk - | VKvalue key -> - try - let _, d = Ephemeron.get key in - if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then - (* v does depend on any of ids, it's ok *) - vk - else - (* v depends on one of the cleared hyps: - we forget the computed value *) - ref VKnone - with Ephemeron.InvalidKey -> ref VKnone + let check_value vk = match force_lazy_val vk with + | None -> vk + | Some (_, d) -> + if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then + (* v does depend on any of ids, it's ok *) + vk + else + (* v depends on one of the cleared hyps: + we forget the computed value *) + dummy_lazy_val () in remove_hyps ids check_context check_value hyps in |