diff options
| author | Pierre-Marie Pédrot | 2019-05-13 00:03:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-14 20:19:37 +0200 |
| commit | e74fce3090323b4d3734f84ee8cf6dc1f5e85953 (patch) | |
| tree | 4c738543dd88e68759fe9c198f0c48d12e73c4e4 /vernac | |
| parent | 106a7c4a86e4c164a73cbc5a4c14f3c4ff527f30 (diff) | |
Abstract away the implementation of side-effects in Safe_typing.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1c7cc5e636..fe895098c0 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -75,13 +75,7 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) 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 env = Safe_typing.push_private_constants env eff in let indexes = search_guard env possible_indexes fixdecls in |