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.

1 files changed, 2 insertions, 4 deletions

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