Further cleaning of the side-effect API.

We remove internal functions and types from the API.

1 files changed, 7 insertions, 9 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1b086d69cc..880a11becd 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -71,15 +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 } ->
-                let fold acc eff = add eff.seff_constant eff.seff_body acc in
-                List.fold_left fold env eff)
-                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