diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 18 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
2 files changed, 9 insertions, 13 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ce74f2344a..880a11becd 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -71,17 +71,13 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let add c cb e = - let exists c e = - try ignore(Environ.lookup_constant c e); true - with Not_found -> false in - if exists c e then e else Environ.add_constant c cb e in - let env = List.fold_left (fun env { eff } -> - match eff with - | SEsubproof (c, cb,_) -> add c cb env - | SEscheme (l,_) -> - List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Safe_typing.side_effects_of_private_constants eff) in + let fold env eff = + try + let _ = Environ.lookup_constant eff.seff_constant env in + env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env + in + let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in let indexes = search_guard env possible_indexes fixdecls in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5258ab2ea4..e1c9712135 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1505,8 +1505,8 @@ let _ = { optdepr = false; optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; - optread = (fun () -> !CClosure.share); - optwrite = (fun b -> CClosure.share := b) } + optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); + optwrite = (fun b -> Global.set_reduction_sharing b) } let _ = declare_bool_option |