From 568f3b69d407f7b5a47d1fdd6ca2bbf3edb5be72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 May 2018 14:51:49 +0200
Subject: Further cleaning of the side-effect API.

We remove internal functions and types from the API.
---
 vernac/lemmas.ml | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

(limited to 'vernac')

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