Merge PR #10151: Clean up the API for side-effects

Reviewed-by: SkySkimmer
Ack-by: gares

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