diff options
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 2dae0ad125..317cf487cc 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 |