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.
---
 proofs/refine.ml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refine.ml b/proofs/refine.ml
index b64e7a2e5e..05d5eaa9e9 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -49,17 +49,14 @@ let (pr_constrv,pr_constr) =
 
 (* Get the side-effect's constant declarations to update the monad's
   * environmnent *)
-let add_if_undefined kn cb env =
-  try ignore(Environ.lookup_constant kn env); env
-  with Not_found -> Environ.add_constant kn cb env
+let add_if_undefined env eff =
+  let open Entries in
+  try ignore(Environ.lookup_constant eff.seff_constant env); env
+  with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
 
 (* Add the side effects to the monad's environment, if not already done. *)
-let add_side_effect env = function
-  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
-    add_if_undefined kn cb env
-  | { Entries.eff = Entries.SEscheme (l,_) } ->
-    List.fold_left (fun env (_,kn,cb,eff_env) ->
-        add_if_undefined kn cb env) env l
+let add_side_effect env { Entries.eff } =
+  List.fold_left add_if_undefined env eff
 
 let add_side_effects env effects =
   List.fold_left (fun env eff -> add_side_effect env eff) env effects
-- 
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.
---
 proofs/refine.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refine.ml b/proofs/refine.ml
index 05d5eaa9e9..198e057ebc 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -55,12 +55,9 @@ let add_if_undefined env eff =
   with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
 
 (* Add the side effects to the monad's environment, if not already done. *)
-let add_side_effect env { Entries.eff } =
+let add_side_effects env eff =
   List.fold_left add_if_undefined env eff
 
-let add_side_effects env effects =
-  List.fold_left (fun env eff -> add_side_effect env eff) env effects
-
 let generic_refine ~typecheck f gl =
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
-- 
cgit v1.2.3