From e74fce3090323b4d3734f84ee8cf6dc1f5e85953 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 May 2019 00:03:36 +0200
Subject: Abstract away the implementation of side-effects in Safe_typing.

---
 vernac/lemmas.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3