From e42b3b188b365159a60851bb0d4214068bb74dd4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 May 2018 11:16:32 +0200
Subject: Share the role type between the implementations of side-effects.

We simply exploit a type isomorphism to remove the use of dedicated algebraic
types in the kernel which are actually not necessary.
---
 vernac/lemmas.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index ce74f2344a..1b086d69cc 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -77,10 +77,8 @@ let adjust_guardness_conditions const = function
                   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 } ->
-                match eff with
-                | SEsubproof (c, cb,_) -> add c cb env
-                | SEscheme (l,_) ->
-                    List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
+                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 indexes =
                 search_guard env
-- 
cgit v1.2.3


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